deffunc H₁( Nat) -> set = 1 / (b to_power ($1 !));
thus ( ex f being Real_Sequence st
for n being Nat holds f . n = H₁(n) & ( for f1, f2 being Real_Sequence st ( for n being Nat holds f1 . n = H₁(n) ) & ( for n being Nat holds f2 . n = H₁(n) ) holds
f1 = f2 ) ) from IRRAT_1:sch 1(); :: thesis: verum