thus
ex seq being Real_Sequence st

for n being Nat holds seq . n = F_{1}(n)
from SEQ_1:sch 1(); :: thesis: for seq1, seq2 being Real_Sequence st ( for n being Nat holds seq1 . n = F_{1}(n) ) & ( for n being Nat holds seq2 . n = F_{1}(n) ) holds

seq1 = seq2

let seq1, seq2 be Real_Sequence; :: thesis: ( ( for n being Nat holds seq1 . n = F_{1}(n) ) & ( for n being Nat holds seq2 . n = F_{1}(n) ) implies seq1 = seq2 )

assume A1: for n being Nat holds seq1 . n = F_{1}(n)
; :: thesis: ( ex n being Nat st not seq2 . n = F_{1}(n) or seq1 = seq2 )

assume A2: for n being Nat holds seq2 . n = F_{1}(n)
; :: thesis: seq1 = seq2

for n being Nat holds seq . n = F

seq1 = seq2

let seq1, seq2 be Real_Sequence; :: thesis: ( ( for n being Nat holds seq1 . n = F

assume A1: for n being Nat holds seq1 . n = F

assume A2: for n being Nat holds seq2 . n = F

now :: thesis: for n being Element of NAT holds seq1 . n = seq2 . n

hence
seq1 = seq2
by FUNCT_2:63; :: thesis: verumlet n be Element of NAT ; :: thesis: seq1 . n = seq2 . n

thus seq1 . n = F_{1}(n)
by A1

.= seq2 . n by A2 ; :: thesis: verum

end;thus seq1 . n = F

.= seq2 . n by A2 ; :: thesis: verum