deffunc H₁( object ) -> set = 0 ;
A1: for a being object st a in T holds
H₁(a) in NAT by ORDINAL1:def 12;
consider f being Function of T,NAT such that
A2: for a being object st a in T holds
f . a = H₁(a) from FUNCT_2:sch 2(A1);
take f ; :: thesis: ex a being object st
( a in T & f . a = 0 )
take a = the Element of T; :: thesis: ( a in T & f . a = 0 )
thus ( a in T & f . a = 0 ) by A2; :: thesis: verum