let a be NAT -valued positive-yielding Real_Sequence; :: thesis: for b being non trivial Nat
for n being non zero Nat holds (Liouville_seq (a,b)) . n > 0
let b be non trivial Nat; :: thesis: for n being non zero Nat holds (Liouville_seq (a,b)) . n > 0
let n be non zero Nat; :: thesis: (Liouville_seq (a,b)) . n > 0
A1: (Liouville_seq (a,b)) . n = (a . n) / (b to_power (n !)) by DefLio;
n in NAT by ORDINAL1:def 12;
then n in dom a by FUNCT_2:def 1;
then a . n in rng a by FUNCT_1:3;
then a . n > 0 by PARTFUN3:def 1;
hence (Liouville_seq (a,b)) . n > 0 by A1; :: thesis: verum