deffunc H₁( Element of NAT ) -> set = Funcs (X . ($1 + 1)),(X . $1);
consider f being ManySortedSet of 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 13;
hence f . n = Funcs (X . (n + 1)),(X . n) by A1; :: thesis: verum