thus ex seq being Real_Sequence st
for n being Nat holds seq . n = F₁(n) from SEQ_1:sch 1(); :: thesis: 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
let seq1, seq2 be Real_Sequence; :: thesis: ( ( for n being Nat holds seq1 . n = F₁(n) ) & ( for n being Nat holds seq2 . n = F₁(n) ) implies seq1 = seq2 )
assume A1: for n being Nat holds seq1 . n = F₁(n) ; :: thesis: ( ex n being Nat st not seq2 . n = F₁(n) or seq1 = seq2 )
assume A2: for n being Nat holds seq2 . n = F₁(n) ; :: thesis: seq1 = seq2

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

let n be Element of NAT ; :: thesis: seq1 . n = seq2 . n
thus seq1 . n = F₁(n) by A1
.= seq2 . n by A2 ; :: thesis: verum

end;

hence seq1 = seq2 by FUNCT_2:63; :: thesis: verum