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

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