set f = BLiouville_seq b;
let x be object ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not x in rng (BLiouville_seq b) or x in NAT )
assume x in rng (BLiouville_seq b) ; :: thesis: x in NAT
then consider n being object such that
AB: ( n in dom (BLiouville_seq b) & x = (BLiouville_seq b) . n ) by FUNCT_1:def 3;
reconsider n = n as Nat by AB;
(BLiouville_seq b) . n = b to_power (n !) by LiuSeq;
hence x in NAT by AB; :: thesis: verum