let A3, A4 be SetSequence of X; :: thesis: ( ( for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) ) & ( for n being Element of NAT holds A4 . n = (A1 . n) /\ (A2 . n) ) implies A3 = A4 )
assume that
A1: for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) and
A2: for n being Element of NAT holds A4 . n = (A1 . n) /\ (A2 . n) ; :: thesis: A3 = A4

now

let n be Element of NAT ; :: thesis: A3 . n = A4 . n
thus A3 . n = (A1 . n) /\ (A2 . n) by A1
.= A4 . n by A2 ; :: thesis: verum

end;

hence A3 = A4 by FUNCT_2:113; :: thesis: verum