let F1, F2 be Functional_Sequence of X1,Y; :: thesis: ( ( for n being Nat holds F1 . n = ProjPMap2 ((F . n),y) ) & ( for n being Nat holds F2 . n = ProjPMap2 ((F . n),y) ) implies F1 = F2 )
assume that
A1: for n being Nat holds F1 . n = ProjPMap2 ((F . n),y) and
A2: for n being Nat holds F2 . n = ProjPMap2 ((F . n),y) ; :: thesis: F1 = F2

now :: thesis: for n being Element of NAT holds F1 . n = F2 . n

let n be Element of NAT ; :: thesis: F1 . n = F2 . n
F1 . n = ProjPMap2 ((F . n),y) by A1;
hence F1 . n = F2 . n by A2; :: thesis: verum

end;

hence F1 = F2 by FUNCT_2:def 8; :: thesis: verum