deffunc H₁( 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₁(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