let f, g be Function; :: thesis: for x, y being object holds (f +* g) +~ (x,y) = (f +~ (x,y)) +* (g +~ (x,y))
let x, y be object ; :: thesis: (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 ;
:: thesis: verum