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
A2: for n being Nat holds it1 . n = (S . n) `1 and
A3: 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 i9 = i as Nat ;
thus it1 . i = (S . i9) `1 by A2
.= it2 . i by A3 ; :: thesis: verum

end;

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