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

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