let f1, f2 be sequence of NAT; ( ( for x being Nat holds f1 . x = F1(x) ) & ( for x being Nat holds f2 . x = F1(x) ) implies f1 = f2 )
assume that
A1:
for x being Nat holds f1 . x = F1(x)
and
A2:
for x being Nat holds f2 . x = F1(x)
; f1 = f2
hence
f1 = f2
by FUNCT_2:63; verum