consider seq being Real_Sequence such that
A1:
for n being Nat holds seq . n = F1(n)
from SEQ_1:sch 1();
thus
ex seq being Real_Sequence st
for n being Nat holds seq . n = F1(n)
by A1; 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 that
A2:
for n being Nat holds seq1 . n = F1(n)
and
A3:
for n being Nat holds seq2 . n = F1(n)
; seq1 = seq2
let n be Element of NAT ; FUNCT_2:def 8 seq1 . n = seq2 . n
thus seq1 . n =
F1(n)
by A2
.=
seq2 . n
by A3
; verum