deffunc H_{1}( Nat) -> set = 1 / (b to_power ($1 !));

thus ( ex f being Real_Sequence st

for n being Nat holds f . n = H_{1}(n) & ( for f1, f2 being Real_Sequence st ( for n being Nat holds f1 . n = H_{1}(n) ) & ( for n being Nat holds f2 . n = H_{1}(n) ) holds

f1 = f2 ) ) from IRRAT_1:sch 1(); :: thesis: verum

thus ( ex f being Real_Sequence st

for n being Nat holds f . n = H

f1 = f2 ) ) from IRRAT_1:sch 1(); :: thesis: verum