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