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;