Attention output is at most the largest value

For all $\htmlData{mx=1}{\iota \in \htmlData{mx=0}{\operatorname{Type}}}$, $\htmlData{mx=1}{d \in \htmlData{mx=0}{\mathbb{N}}}$, $\htmlData{mx=5}{q : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{d}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\mathbb{R}}}$, $\htmlData{mx=7}{K : \htmlData{mx=0}{\iota} \mathrel{\htmlData{mx=6}{\to}} \htmlData{mx=3}{\htmlData{mx=1}{\operatorname{Fin}}\,\htmlData{mx=2}{d}} \mathrel{\htmlData{mx=5}{\to}} \htmlData{mx=4}{\mathbb{R}}}$, $\htmlData{mx=3}{V : \htmlData{mx=0}{\iota} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ and $\htmlData{mx=1}{m \in \htmlData{mx=0}{\mathbb{R}}}$, if $\htmlData{mx=5}{\forall i,\ \htmlData{mx=2}{\htmlData{mx=0}{V}(\htmlData{mx=1}{i})} \mathrel{\htmlData{mx=4}{\leq}} \htmlData{mx=3}{m}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{\iota}}$ and $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Nonempty}}\,\htmlData{mx=1}{\iota}}$), then