let IT, A1 be SetSequence of X; ( ( for n being Nat holds IT . n = (A1 . n) ` ) implies for n being Nat holds A1 . n = (IT . n) ` )
assume A6:
for n being Nat holds IT . n = (A1 . n) `
; for n being Nat holds A1 . n = (IT . n) `
let n be Nat; A1 . n = (IT . n) `
thus A1 . n =
((A1 . n) `) `
.=
(IT . n) `
by A6
; verum