deffunc H_{1}( Nat) -> set = ((BLiouville_seq b) . $1) * (Sum ((Liouville_seq (a,b)) |_ (Seg $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