let it1, it2 be preVNumberingSeq of G; :: thesis: ( ( for n being Nat holds it1 . n = (S . n) `1 ) & ( for n being Nat holds it2 . n = (S . n) `1 ) implies it1 = it2 )
assume that
A1: for n being Nat holds it1 . n = (S . n) `1 and
A2: for n being Nat holds it2 . n = (S . n) `1 ; :: thesis: it1 = it2

now

let i be set ; :: thesis: ( i in NAT implies it1 . i = it2 . i )
assume i in NAT ; :: thesis: it1 . i = it2 . i
then reconsider i' = i as Nat ;
thus it1 . i = (S . i') `1 by A1
.= it2 . i by A2 ; :: thesis: verum

end;

hence it1 = it2 by PBOOLE:3; :: thesis: verum