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 A1: x in {a,b} ; :: thesis: x in rng (a followed_by b)
A2: dom (NAT --> b) = NAT by FUNCOP_1:19;
then 1 in dom (NAT --> b) ;
then A3: 1 in dom (a followed_by b) by Th32;
(a followed_by b) . 1 = b by Th122;
then A4: b in rng (a followed_by b) by A3, FUNCT_1:12;
a in rng (a followed_by b) by A2, Th104;
hence x in rng (a followed_by b) by A1, A4, TARSKI:def 2; :: thesis: verum