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

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