let a, b, c be set ; :: thesis: rng ((a,b) followed_by c) = {a,b,c}
A1: (a,b) followed_by c = (a followed_by c) +* (1,b) by Th124;
then A2: dom ((a,b) followed_by c) = dom (a followed_by c) by Th29
.= dom (NAT --> c) by Th29
.= NAT ;
((a,b) followed_by c) . 2 = c by Th123;
then A3: c in rng ((a,b) followed_by c) by A2, FUNCT_1:3;
((a,b) followed_by c) . 1 = b by Th122;
then A4: b in rng ((a,b) followed_by c) by A2, FUNCT_1:3;
rng (a followed_by c) = {a,c} by Th125;
then rng ((a followed_by c) +* (1,b)) c= {a,c} \/ {b} by Th99;
then rng ((a followed_by c) +* (1,b)) c= {a,c,b} by ENUMSET1:3;
hence rng ((a,b) followed_by c) c= {a,b,c} by A1, ENUMSET1:57; :: according to XBOOLE_0:def 10 :: thesis: {a,b,c} c= rng ((a,b) followed_by c)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {a,b,c} or x in rng ((a,b) followed_by c) )
((a,b) followed_by c) . 0 = a by Th121;
then A5: a in rng ((a,b) followed_by c) by A2, FUNCT_1:3;
assume x in {a,b,c} ; :: thesis: x in rng ((a,b) followed_by c)
hence x in rng ((a,b) followed_by c) by A5, A4, A3, ENUMSET1:def 1; :: thesis: verum