let G1, G2 be Functional_Sequence of X,Y; ( ( 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)
; G1 = G2
for m being Element of NAT holds G1 . m = G2 . m
hence
G1 = G2
; verum