let n, b be non zero Nat; :: thesis: ( b > 1 implies (BLiouville_seq b) . n > 1 )
assume A1: b > 1 ; :: thesis: (BLiouville_seq b) . n > 1
(BLiouville_seq b) . n = b to_power (n !) by LiuSeq;
hence (BLiouville_seq b) . n > 1 by A1, POWER:35; :: thesis: verum