let G1, G2 be Functional_Sequence of X,Y; :: thesis: ( ( for m being Nat holds G1 . m = F . (m,n) ) & ( for m being Nat holds G2 . m = F . (m,n) ) implies G1 = G2 )
assume that
A9: for m being Nat holds G1 . m = F . (m,n) and
A10: for m being Nat holds G2 . m = F . (m,n) ; :: 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 . (m1,n) by A9;
hence G1 . m = G2 . m by A10; :: thesis: verum

end;

hence G1 = G2 ; :: thesis: verum