deffunc H_{1}( Nat) -> set = ($1 choose k) * ($1 ^ (- k));

thus ( ex seq being Real_Sequence st

for n being Nat holds seq . n = H_{1}(n) & ( for seq1, seq2 being Real_Sequence st ( for n being Nat holds seq1 . n = H_{1}(n) ) & ( for n being Nat holds seq2 . n = H_{1}(n) ) holds

seq1 = seq2 ) ) from IRRAT_1:sch 1(); :: thesis: verum

thus ( ex seq being Real_Sequence st

for n being Nat holds seq . n = H

seq1 = seq2 ) ) from IRRAT_1:sch 1(); :: thesis: verum