let a, b be set ; :: thesis: rng (a followed_by b) = {a,b}
rng (NAT --> b) = {b} by FUNCOP_1:14;
then rng ((NAT --> b) +* 0 ,a) c= {b} \/ {a} by Th102;
hence rng (a followed_by b) c= {a,b} by ENUMSET1:41; :: according to XBOOLE_0:def 10 :: thesis: {a,b} c= rng (a followed_by b)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {a,b} or x in rng (a followed_by b) )
assume Z: x in {a,b} ; :: thesis: x in rng (a followed_by b)
X: dom (NAT --> b) = NAT by FUNCOP_1:19;
then A: a in rng (a followed_by b) by Th104;
1 in dom (NAT --> b) by X;
then B: 1 in dom (a followed_by b) by Th32;
(a followed_by b) . 1 = b by Th55;
then b in rng (a followed_by b) by B, FUNCT_1:12;
hence x in rng (a followed_by b) by A, Z, TARSKI:def 2; :: thesis: verum