let a, b, c be set ; 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; XBOOLE_0:def 10 {a,b,c} c= rng ((a,b) followed_by c)
let x be object ; TARSKI:def 3 ( 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}
; x in rng ((a,b) followed_by c)
hence
x in rng ((a,b) followed_by c)
by A5, A4, A3, ENUMSET1:def 1; verum