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;
F: dom (a,b followed_by c) = NAT by Thx;
H: dom (a followed_by c) = NAT by Thy;
hence dom (a,b followed_by c) = dom ((a followed_by c) +* 1,b) by F, 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 F;

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

suppose S: 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 Th57
.= (a followed_by c) . x by S, Th54
.= ((a followed_by c) +* 1,b) . x by S, Th34 ;
:: thesis: verum

end;

suppose S: 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 Th58
.= ((a followed_by c) +* 1,b) . x by S, H, Th33 ;
:: thesis: verum

end;

suppose S: 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 Th59
.= (a followed_by c) . x by S, Th55
.= ((a followed_by c) +* 1,b) . x by S, Th34 ;
:: thesis: verum

end;

end;