A0: rng (seq_const 1) = {1} by FUNCOP_1:8;
A1: 1 in 10 by ENUMSET1:def 8, CARD_1:58;
not 10 is trivial by NAT_2:28;
hence Liouville_constant is liouville by A1, Th38, A0, ZFMISC_1:31; :: thesis: verum