( ex seq being Real_Sequence st
for n being Nat holds seq . n = F₁(n) & ( for seq1, seq2 being Real_Sequence st ( for n being Nat holds seq1 . n = F₁(n) ) & ( for n being Nat holds seq2 . n = F₁(n) ) holds
seq1 = seq2 ) )