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
A4: for m being Nat holds G1 . m = F . (n,m) and
A5: 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 A4;
hence G1 . m = G2 . m by A5; :: thesis: verum

end;

hence G1 = G2 ; :: thesis: verum