let IT, A1 be SetSequence of X; :: thesis: ( ( 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) ` ; :: thesis: for n being Nat holds A1 . n = (IT . n) `

let n be Nat; :: thesis: A1 . n = (IT . n) `

thus A1 . n = ((A1 . n) `) `

.= (IT . n) ` by A6 ; :: thesis: verum

assume A6: for n being Nat holds IT . n = (A1 . n) ` ; :: thesis: for n being Nat holds A1 . n = (IT . n) `

let n be Nat; :: thesis: A1 . n = (IT . n) `

thus A1 . n = ((A1 . n) `) `

.= (IT . n) ` by A6 ; :: thesis: verum