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

now :: thesis: for i being Nat holds f . i is PartFunc of (the_Vertices_of G),NAT

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

end;

then reconsider f = f as preVNumberingSeq of G by Def7;
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 12;
hence f . n = (S . n) `1 by A1; :: thesis: verum