deffunc H1( Element of IIG) -> Nat = depth ($1,A);
set Ds = { H1(v) where v is Element of IIG : v in the carrier of IIG } ;
A1: { H1(v) where v is Element of IIG : v in the carrier of IIG } is natural-membered
proof
let e be object ; :: according to MEMBERED:def 6 :: thesis: ( not e in { H1(v) where v is Element of IIG : v in the carrier of IIG } or not e is V27() )
assume e in { H1(v) where v is Element of IIG : v in the carrier of IIG } ; :: thesis: e is V27()
then ex v being Element of IIG st
( e = depth (v,A) & v in the carrier of IIG ) ;
hence e is V27() ; :: thesis: verum
end;
set v = the Element of IIG;
A2: depth ( the Element of IIG,A) in { H1(v) where v is Element of IIG : v in the carrier of IIG } ;
A3: the carrier of IIG is finite ;
{ H1(v) where v is Element of IIG : v in the carrier of IIG } is finite from FRAENKEL:sch 21(A3);
 then reconsider Ds = { H1(v) where v is Element of IIG : v in the carrier of IIG } as non empty finite Subset of NAT by A1, A2, MEMBERED:6;
reconsider m = max Ds as Nat by TARSKI:1;
take m ; :: thesis: ex Ds being non empty finite Subset of NAT st
( Ds = { (depth (v,A)) where v is Element of IIG : v in the carrier of IIG } & m = max Ds )
take Ds ; :: thesis: ( Ds = { (depth (v,A)) where v is Element of IIG : v in the carrier of IIG } & m = max Ds )
thus ( Ds = { (depth (v,A)) where v is Element of IIG : v in the carrier of IIG } & m = max Ds ) ; :: thesis: verum