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