let a, b be set ; :: thesis: rng (a followed_by b) = {a,b}
rng (NAT --> b) = {b} by FUNCOP_1:8;
then rng ((NAT --> b) +* (0,a)) c= {b} \/ {a} by Th99;
hence rng (a followed_by b) c= {a,b} by ENUMSET1:1; :: according to XBOOLE_0:def 10 :: thesis: {a,b} c= rng (a followed_by b)
let x be object ; :: 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 ;
1 in dom (NAT --> b) ;
then A3: 1 in dom (a followed_by b) by Th29;
(a followed_by b) . 1 = b by Th119;
then A4: b in rng (a followed_by b) by A3, FUNCT_1:3;
a in rng (a followed_by b) by A2, Th101;
hence x in rng (a followed_by b) by A1, A4, TARSKI:def 2; :: thesis: verum