deffunc H₁( Element of the Sorts of (FreeEnv A) . v) -> Element of NAT = card $1;
set s = { H₁(t) where t is Element of the Sorts of (FreeEnv A) . v : S₁[t] } ;
set t = the Element of the Sorts of (FreeEnv A) . v;
A1: card the Element of the Sorts of (FreeEnv A) . v in { H₁(t) where t is Element of the Sorts of (FreeEnv A) . v : S₁[t] } ;
A2: { H₁(t) where t is Element of the Sorts of (FreeEnv A) . v : S₁[t] } is Subset of NAT from DOMAIN_1:sch 8();
{ H₁(t) where t is Element of the Sorts of (FreeEnv A) . v : S₁[t] } is finite from PRE_CIRC:sch 1();
then reconsider s = { H₁(t) where t is Element of the Sorts of (FreeEnv A) . v : S₁[t] } as non empty finite Subset of NAT by A1, A2;
reconsider m = max s as Nat by TARSKI:1;
take m ; :: thesis: ex s being non empty finite Subset of NAT st
( s = { (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & m = max s )
take s ; :: thesis: ( s = { (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & m = max s )
thus ( s = { (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & m = max s ) ; :: thesis: verum