let x, y be object ; :: thesis: for f, g being Function holds (Swap (f,x,y)) * g = Swap ((f * g),x,y)
let f, g be Function; :: thesis: (Swap (f,x,y)) * g = Swap ((f * g),x,y)
set S = Swap (f,x,y);
set Sg = Swap ((f * g),x,y);
A1: ( dom (Swap (f,x,y)) = dom f & dom (Swap ((f * g),x,y)) = dom (f * g) ) by Def4;
A2: dom ((Swap (f,x,y)) * g) c= dom (f * g)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in dom ((Swap (f,x,y)) * g) or a in dom (f * g) )
assume a in dom ((Swap (f,x,y)) * g) ; :: thesis: a in dom (f * g)
then ( a in dom g & g . a in dom (Swap (f,x,y)) ) by FUNCT_1:11;
hence a in dom (f * g) by A1, FUNCT_1:11; :: thesis: verum

end;

dom (f * g) c= dom ((Swap (f,x,y)) * g)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in dom (f * g) or a in dom ((Swap (f,x,y)) * g) )
assume a in dom (f * g) ; :: thesis: a in dom ((Swap (f,x,y)) * g)
then ( a in dom g & g . a in dom f ) by FUNCT_1:11;
hence a in dom ((Swap (f,x,y)) * g) by A1, FUNCT_1:11; :: thesis: verum

end;

then A3: dom (Swap ((f * g),x,y)) = dom ((Swap (f,x,y)) * g) by A2, Def4;
for a being object st a in dom (Swap ((f * g),x,y)) holds
(Swap ((f * g),x,y)) . a = ((Swap (f,x,y)) * g) . a

proof

let a be object ; :: thesis: ( a in dom (Swap ((f * g),x,y)) implies (Swap ((f * g),x,y)) . a = ((Swap (f,x,y)) * g) . a )
assume A4: a in dom (Swap ((f * g),x,y)) ; :: thesis: (Swap ((f * g),x,y)) . a = ((Swap (f,x,y)) * g) . a
A5: a in dom (f * g) by A4, Def4;
then A6: (f * g) . a = f . (g . a) by FUNCT_1:12;
A7: ( ((Swap (f,x,y)) * g) . a = (Swap (f,x,y)) . (g . a) & g . a in dom (Swap (f,x,y)) ) by A4, A3, FUNCT_1:11, FUNCT_1:12;

per cases ( x in (f * g) . a or not x in (f * g) . a ) ;

suppose A8: x in (f * g) . a ; :: thesis: (Swap ((f * g),x,y)) . a = ((Swap (f,x,y)) * g) . a

then (Swap ((f * g),x,y)) . a = (((f * g) . a) \ {x}) \/ {y} by A5, Def4;
hence (Swap ((f * g),x,y)) . a = ((Swap (f,x,y)) * g) . a by A6, A7, A8, A1, Def4; :: thesis: verum

end;

suppose A9: not x in (f * g) . a ; :: thesis: (Swap ((f * g),x,y)) . a = ((Swap (f,x,y)) * g) . a

then (Swap ((f * g),x,y)) . a = ((f * g) . a) \/ {x} by A5, Def4;
hence (Swap ((f * g),x,y)) . a = ((Swap (f,x,y)) * g) . a by A9, A6, A7, A1, Def4; :: thesis: verum

end;

end;

end;

hence (Swap (f,x,y)) * g = Swap ((f * g),x,y) by A3; :: thesis: verum