thus
ex seq being Real_Sequence st
for n being Nat holds seq . n = F1(n)
from SEQ_1:sch 1(); for seq1, seq2 being Real_Sequence st ( for n being Nat holds seq1 . n = F1(n) ) & ( for n being Nat holds seq2 . n = F1(n) ) holds
seq1 = seq2
let seq1, seq2 be Real_Sequence; ( ( for n being Nat holds seq1 . n = F1(n) ) & ( for n being Nat holds seq2 . n = F1(n) ) implies seq1 = seq2 )
assume A1:
for n being Nat holds seq1 . n = F1(n)
; ( ex n being Nat st not seq2 . n = F1(n) or seq1 = seq2 )
assume A2:
for n being Nat holds seq2 . n = F1(n)
; seq1 = seq2
hence
seq1 = seq2
by FUNCT_2:63; verum