let a be NAT -valued Real_Sequence; :: thesis: for b being non trivial Nat
for n being Nat holds (Liouville_seq (a,b)) . n >= 0
let b be non trivial Nat; :: thesis: for n being Nat holds (Liouville_seq (a,b)) . n >= 0
let n be Nat; :: thesis: (Liouville_seq (a,b)) . n >= 0
per cases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; :: thesis: (Liouville_seq (a,b)) . n >= 0
hence (Liouville_seq (a,b)) . n >= 0 by DefLio; :: thesis: verum
end;
suppose n <> 0 ; :: thesis: (Liouville_seq (a,b)) . n >= 0
then (Liouville_seq (a,b)) . n = (a . n) / (b to_power (n !)) by DefLio;
hence (Liouville_seq (a,b)) . n >= 0 ; :: thesis: verum
end;
end;