let a, b, c be set ; :: thesis: a,b followed_by c = (a followed_by c) +* 1,b
set f = a,b followed_by c;
set g = (a followed_by c) +* 1,b;
A1: dom (a followed_by c) = NAT by Th120;
A2: dom (a,b followed_by c) = NAT by Th123;
hence dom (a,b followed_by c) = dom ((a followed_by c) +* 1,b) by A1, Th32; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in proj1 (a,b followed_by c) or (a,b followed_by c) . b₁ = ((a followed_by c) +* 1,b) . b₁ )
let x be set ; :: thesis: ( not x in proj1 (a,b followed_by c) or (a,b followed_by c) . x = ((a followed_by c) +* 1,b) . x )
assume x in dom (a,b followed_by c) ; :: thesis: (a,b followed_by c) . x = ((a followed_by c) +* 1,b) . x
then reconsider n = x as Nat by A2;

per cases ( n = 0 or n = 1 or n > 1 ) by NAT_1:26;

suppose A3: n = 0 ; :: thesis: (a,b followed_by c) . x = ((a followed_by c) +* 1,b) . x

hence (a,b followed_by c) . x = a by Th124
.= (a followed_by c) . x by A3, Th121
.= ((a followed_by c) +* 1,b) . x by A3, Th34 ;
:: thesis: verum

end;

suppose A4: n = 1 ; :: thesis: (a,b followed_by c) . x = ((a followed_by c) +* 1,b) . x

hence (a,b followed_by c) . x = b by Th125
.= ((a followed_by c) +* 1,b) . x by A1, A4, Th33 ;
:: thesis: verum

end;

suppose A5: n > 1 ; :: thesis: (a,b followed_by c) . x = ((a followed_by c) +* 1,b) . x

hence (a,b followed_by c) . x = c by Th126
.= (a followed_by c) . x by A5, Th122
.= ((a followed_by c) +* 1,b) . x by A5, Th34 ;
:: thesis: verum

end;

end;