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;