deffunc H_{1}( Nat) -> set = meet { (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_{1}(n) ) )
from FUNCT_1:sch 4();

take f ; :: thesis: ( dom f = NAT & ( for n being Nat holds f . n = meet { (B . k) where k is Nat : n <= k } ) )

thus dom f = NAT by A1; :: thesis: for n being Nat holds f . n = meet { (B . k) where k is Nat : n <= k }

let n be Nat; :: thesis: f . n = meet { (B . k) where k is Nat : n <= k }

n in NAT by ORDINAL1:def 12;

hence f . n = meet { (B . k) where k is Nat : n <= k } by A1; :: thesis: verum

consider f being Function such that

A1: ( dom f = NAT & ( for n being Element of NAT holds f . n = H

take f ; :: thesis: ( dom f = NAT & ( for n being Nat holds f . n = meet { (B . k) where k is Nat : n <= k } ) )

thus dom f = NAT by A1; :: thesis: for n being Nat holds f . n = meet { (B . k) where k is Nat : n <= k }

let n be Nat; :: thesis: f . n = meet { (B . k) where k is Nat : n <= k }

n in NAT by ORDINAL1:def 12;

hence f . n = meet { (B . k) where k is Nat : n <= k } by A1; :: thesis: verum