let A3, A4 be SetSequence of X; :: thesis: ( ( for n being Element of NAT holds A3 . n = (A1 . n) \ A ) & ( for n being Element of NAT holds A4 . n = (A1 . n) \ A ) implies A3 = A4 )
assume that
A7: for n being Element of NAT holds A3 . n = (A1 . n) \ A and
A8: for n being Element of NAT holds A4 . n = (A1 . n) \ A ; :: thesis: A3 = A4
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: A3 . n = A4 . n
thus A3 . n = (A1 . n) \ A by A7
.= A4 . n by A8 ; :: thesis: verum