deffunc H_{1}( Element of NAT ) -> set = Funcs ((X . ($1 + 1)),(X . $1));

consider f being ManySortedSet of NAT such that

A1: for n being Element of NAT holds f . n = H_{1}(n)
from PBOOLE:sch 5();

reconsider f = f as SetSequence ;

take f ; :: thesis: for n being Nat holds f . n = Funcs ((X . (n + 1)),(X . n))

let n be Nat; :: thesis: f . n = Funcs ((X . (n + 1)),(X . n))

n in NAT by ORDINAL1:def 12;

hence f . n = Funcs ((X . (n + 1)),(X . n)) by A1; :: thesis: verum

consider f being ManySortedSet of NAT such that

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

reconsider f = f as SetSequence ;

take f ; :: thesis: for n being Nat holds f . n = Funcs ((X . (n + 1)),(X . n))

let n be Nat; :: thesis: f . n = Funcs ((X . (n + 1)),(X . n))

n in NAT by ORDINAL1:def 12;

hence f . n = Funcs ((X . (n + 1)),(X . n)) by A1; :: thesis: verum