deffunc H₁( object ) -> object = ((transitions_of (x,Inv)) . $1) `1 ;
consider f being Function such that
A1: dom f = NAT and
A2: for x being object st x in NAT holds
f . x = H<sub>1</sub>(x) from FUNCT_1:sch 3();
take f ; :: thesis: ( dom f = NAT & ( for k being Nat holds f . k = ((transitions_of (x,Inv)) . k) `1 ) )
thus ( dom f = NAT & ( for k being Nat holds f . k = ((transitions_of (x,Inv)) . k) `1 ) ) by A1, A2, ORDINAL1:def 12; :: thesis: verum