deffunc H_{1}( 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_{1}(i)
from PBOOLE:sch 4();

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

consider f being ManySortedSet of NAT such that

A1: for i being object st i in NAT holds

f . i = H

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

then reconsider f = f as preVNumberingSeq of G by Def7;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;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

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