let G1, G2 be Functional_Sequence of X,Y; :: thesis: ( ( for m being Nat holds G1 . m = F . n,m ) & ( for m being Nat holds G2 . m = F . n,m ) implies G1 = G2 )
assume that
A1: for m being Nat holds G1 . m = F . n,m and
A2: for m being Nat holds G2 . m = F . n,m ; :: thesis: G1 = G2
for m being Element of NAT holds G1 . m = G2 . m

proof

let m be Element of NAT ; :: thesis: G1 . m = G2 . m
reconsider m1 = m as Nat ;
G1 . m = F . n,m1 by A1;
hence G1 . m = G2 . m by A2; :: thesis: verum

end;

hence G1 = G2 by FUNCT_2:113; :: thesis: verum