( ex seq being Real_Sequence st for n being Element of NAT holds seq . n = F1(n) & ( for seq1, seq2 being Real_Sequence st ( for n being Element of NAT holds seq1 . n = F1(n) ) & ( for n being Element of NAT holds seq2 . n = F1(n) ) holds seq1 = seq2 ) )