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

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 :: thesis: for i being object st i in NAT holds

it1 . i = it2 . i

hence
it1 = it2
by PBOOLE:3; :: thesis: verumit1 . i = it2 . i

let i be object ; :: 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;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