let f, g be Function; for x, y being object holds (f +* g) +~ (x,y) = (f +~ (x,y)) +* (g +~ (x,y))
let x, y be object ; (f +* g) +~ (x,y) = (f +~ (x,y)) +* (g +~ (x,y))
set A = (rng f) \/ (rng g);
A1:
g +~ (x,y) = ((id ((rng f) \/ (rng g))) +* (x,y)) * g
by Th115, XBOOLE_1:7;
A2: dom ((id ((rng f) \/ (rng g))) +* (x,y)) =
dom (id ((rng f) \/ (rng g)))
by Th29
.=
(rng f) \/ (rng g)
;
rng (f +* g) c= (rng f) \/ (rng g)
by FUNCT_4:17;
hence (f +* g) +~ (x,y) =
((id ((rng f) \/ (rng g))) +* (x,y)) * (f +* g)
by Th115
.=
(((id ((rng f) \/ (rng g))) +* (x,y)) * f) +* (((id ((rng f) \/ (rng g))) +* (x,y)) * g)
by A2, Th9, XBOOLE_1:7
.=
(f +~ (x,y)) +* (g +~ (x,y))
by A1, Th115, XBOOLE_1:7
;
verum