deffunc H₁( Nat) -> set = union { (B . k) where k is Nat : $1 <= k } ;
consider f being Function such that
A1: ( dom f = NAT & ( for n being Element of NAT holds f . n = H₁(n) ) ) from FUNCT_1:sch 4();
take f ; :: thesis: ( dom f = NAT & ( for n being Nat holds f . n = union { (B . k) where k is Nat : n <= k } ) )
thus dom f = NAT by A1; :: thesis: for n being Nat holds f . n = union { (B . k) where k is Nat : n <= k }
let n be Nat; :: thesis: f . n = union { (B . k) where k is Nat : n <= k }
n in NAT by ORDINAL1:def 12;
hence f . n = union { (B . k) where k is Nat : n <= k } by A1; :: thesis: verum