deffunc H₁( Nat) -> Element of Trivial-SigmaField REAL = {(In ($1,NAT))};
AA: for x being Element of NAT holds H₁(x) in bool NAT

proof

let x be Element of NAT ; :: thesis: H₁(x) in bool NAT
H₁(x) c= NAT by ZFMISC_1:31;
hence H₁(x) in bool NAT ; :: thesis: verum

end;

consider f being SetSequence of NAT such that
A1: for d being Element of NAT holds f . d = H₁(d) from FUNCT_2:sch 8(AA);
take f ; :: thesis: for n being Nat holds f . n = {n}
let n be Nat; :: thesis: f . n = {n}
reconsider n = n as Element of NAT by ORDINAL1:def 12;
f . n = H₁(n) by A1;
hence f . n = {n} ; :: thesis: verum