let a, b, c be set ; (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; FUNCT_1:def 11 for b1 being object holds
( not b1 in proj1 ((a,b) followed_by c) or ((a,b) followed_by c) . b1 = ((a followed_by c) +* (1,b)) . b1 )
let x be object ; ( 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)
; ((a,b) followed_by c) . x = ((a followed_by c) +* (1,b)) . x
then reconsider n = x as Nat by A2;