deffunc H₁( Element of NAT ) -> Element of the carrier of (TOP-REAL N) = (seq1 . $1) + (seq2 . $1);
thus ex s being Real_Sequence of N st
for n being Element of NAT holds s . n = H₁(n) from FUNCT_2:sch 4(); :: thesis: verum