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 Th117;
A2: dom ((a,b) followed_by c) = NAT by Th120;
hence dom ((a,b) followed_by c) = dom ((a followed_by c) +* (1,b)) by A1, Th29; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object 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 object ; :: 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:25;

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 Th121
.= (a followed_by c) . x by A3, Th118
.= ((a followed_by c) +* (1,b)) . x by A3, Th31 ;
:: 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 Th122
.= ((a followed_by c) +* (1,b)) . x by A1, A4, Th30 ;
:: 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 Th123
.= (a followed_by c) . x by A5, Th119
.= ((a followed_by c) +* (1,b)) . x by A5, Th31 ;
:: thesis: verum

end;

end;