let a be Real_Sequence; :: thesis: for n, b being non zero Nat st b > 1 holds
((ALiouville_seq (a,b)) . n) / ((BLiouville_seq b) . n) = Sum (FinSeq ((Liouville_seq (a,b)),n))
let n, b be non zero Nat; :: thesis: ( b > 1 implies ((ALiouville_seq (a,b)) . n) / ((BLiouville_seq b) . n) = Sum (FinSeq ((Liouville_seq (a,b)),n)) )
assume b > 1 ; :: thesis: ((ALiouville_seq (a,b)) . n) / ((BLiouville_seq b) . n) = Sum (FinSeq ((Liouville_seq (a,b)),n))
then A1: (BLiouville_seq b) . n <> 0 by Th30;
A2: (Liouville_seq (a,b)) . 0 = 0 by DefLio;
thus ((ALiouville_seq (a,b)) . n) / ((BLiouville_seq b) . n) = (((BLiouville_seq b) . n) * (Sum ((Liouville_seq (a,b)) |_ (Seg n)))) / ((BLiouville_seq b) . n) by ALiuDef
.= Sum ((Liouville_seq (a,b)) |_ (Seg n)) by XCMPLX_1:89, A1
.= Sum (FinSeq ((Liouville_seq (a,b)),n)) by Th18, A2 ; :: thesis: verum