let g, h, f be Function; :: thesis: ( dom g misses dom h implies (f \ g) +* h = (f +* h) \ g )
assume A1: dom g misses dom h ; :: thesis: (f \ g) +* h = (f +* h) \ g
A2: dom (f +* h) = (dom f) \/ (dom h) by Def1;
A3: dom ((f \ g) +* h) = (dom (f \ g)) \/ (dom h) by Def1;
A4: dom ((f \ g) +* h) = dom ((f +* h) \ g)

proof

thus dom ((f \ g) +* h) c= dom ((f +* h) \ g) :: according to XBOOLE_0:def 10 :: thesis: dom ((f +* h) \ g) c= dom ((f \ g) +* h)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((f \ g) +* h) or x in dom ((f +* h) \ g) )
assume A5: x in dom ((f \ g) +* h) ; :: thesis: x in dom ((f +* h) \ g)

per cases ( ( x in dom (f \ g) & not x in dom h ) or x in dom h ) by A3, A5, XBOOLE_0:def 3;

suppose that A6: x in dom (f \ g) and
A7: not x in dom h ; :: thesis: x in dom ((f +* h) \ g)

consider y being set such that
A8: [x,y] in f \ g by A6, RELAT_1:def 4;
A9: x in dom f by A8, RELAT_1:def 4;
then A10: x in dom (f +* h) by A2, XBOOLE_0:def 3;
A11: not [x,y] in g by A8, XBOOLE_0:def 5;
A12: (f +* h) . x = f . x by A7, Th12;
f . x = y by A8, A9, FUNCT_1:def 2;
then [x,y] in f +* h by A12, A10, FUNCT_1:def 2;
then [x,y] in (f +* h) \ g by A11, XBOOLE_0:def 5;
hence x in dom ((f +* h) \ g) by RELAT_1:def 4; :: thesis: verum

end;

suppose A13: x in dom h ; :: thesis: x in dom ((f +* h) \ g)

then A14: not x in dom g by A1, XBOOLE_0:3;
x in dom (f +* h) by A2, A13, XBOOLE_0:def 3;
then A15: x in (dom (f +* h)) \ (dom g) by A14, XBOOLE_0:def 5;
(dom (f +* h)) \ (dom g) c= dom ((f +* h) \ g) by RELAT_1:3;
hence x in dom ((f +* h) \ g) by A15; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((f +* h) \ g) or x in dom ((f \ g) +* h) )
assume x in dom ((f +* h) \ g) ; :: thesis: x in dom ((f \ g) +* h)
then consider y being set such that
A16: [x,y] in (f +* h) \ g by RELAT_1:def 4;
A17: x in dom (f +* h) by A16, RELAT_1:def 4;
then A18: y = (f +* h) . x by A16, FUNCT_1:def 2;

per cases ( ( x in dom f & not x in dom h ) or x in dom h ) by A2, A17, XBOOLE_0:def 3;

suppose that A19: x in dom f and
A20: not x in dom h ; :: thesis: x in dom ((f \ g) +* h)

A21: not [x,y] in g by A16, XBOOLE_0:def 5;
(f +* h) . x = f . x by A20, Th12;
then [x,y] in f by A19, A18, FUNCT_1:def 2;
then [x,y] in f \ g by A21, XBOOLE_0:def 5;
then x in dom (f \ g) by RELAT_1:def 4;
hence x in dom ((f \ g) +* h) by A3, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x in dom h ; :: thesis: x in dom ((f \ g) +* h)

hence x in dom ((f \ g) +* h) by A3, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

now

let x be set ; :: thesis: ( x in dom ((f \ g) +* h) implies ((f \ g) +* h) . b₁ = ((f +* h) \ g) . b₁ )
assume A22: x in dom ((f \ g) +* h) ; :: thesis: ((f \ g) +* h) . b₁ = ((f +* h) \ g) . b₁

per cases ( ( x in dom (f \ g) & not x in dom h ) or x in dom h ) by A3, A22, XBOOLE_0:def 3;

suppose that A23: x in dom (f \ g) and
A24: not x in dom h ; :: thesis: ((f \ g) +* h) . b₁ = ((f +* h) \ g) . b₁

thus ((f \ g) +* h) . x = (f \ g) . x by A24, Th12
.= f . x by A23, GRFUNC_1:2
.= (f +* h) . x by A24, Th12
.= ((f +* h) \ g) . x by A4, A22, GRFUNC_1:2 ; :: thesis: verum

end;

suppose A25: x in dom h ; :: thesis: ((f +* h) \ g) . b₁ = ((f \ g) +* h) . b₁

then A26: not x in dom g by A1, XBOOLE_0:3;
x in dom (f +* h) by A25, A2, XBOOLE_0:def 3;
then x in (dom (f +* h)) \ (dom g) by A26, XBOOLE_0:def 5;
hence ((f +* h) \ g) . x = (f +* h) . x by GRFUNC_1:32
.= h . x by A25, Th14
.= ((f \ g) +* h) . x by A25, Th14 ;
:: thesis: verum

end;

end;

end;

hence (f \ g) +* h = (f +* h) \ g by A4, FUNCT_1:2; :: thesis: verum