deffunc H1( Nat) -> set = 2 -(2 /($1 + 1)); thus
( ex seq being Real_Sequence st for n being Nat holds seq . n = H1(n) & ( for seq1, seq2 being Real_Sequence st ( for n being Nat holds seq1 . n = H1(n) ) & ( for n being Nat holds seq2 . n = H1(n) ) holds seq1 = seq2 ) )
fromNUMPOLY1:sch 1();:: thesis: verum