deffunc H₁( 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₁(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