deffunc H₁( set ) -> set = (S . $1) `1 ;
consider f being ManySortedSet of NAT such that
A1: for i being set st i in NAT holds
f . i = H₁(i) from PBOOLE:sch 4();

now

let i be Nat; :: thesis: f . i is PartFunc of ,
i in NAT by ORDINAL1:def 13;
then f . i = (S . i) `1 by A1;
hence f . i is PartFunc of , ; :: thesis: verum

end;

then reconsider f = f as preVNumberingSeq of G by Def8;
take f ; :: thesis: for n being Nat holds f . n = (S . n) `1
let n be Nat; :: thesis: f . n = (S . n) `1
n in NAT by ORDINAL1:def 13;
hence f . n = (S . n) `1 by A1; :: thesis: verum