deffunc H1( Nat) -> set = 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 ) )
fromIRRAT_1:sch 1();:: thesis: verum