let f, g be Function; :: thesis: for x, y being set holds (f +* g) +~ (x,y) = (f +~ (x,y)) +* (g +~ (x,y))
let x, y be set ; :: 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 Th118, XBOOLE_1:7;
A2: dom ((id ((rng f) \/ (rng g))) +* (x,y)) = dom (id ((rng f) \/ (rng g))) by Th32
.= (rng f) \/ (rng g) by RELAT_1:45 ;
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 Th118
.= (((id ((rng f) \/ (rng g))) +* (x,y)) * f) +* (((id ((rng f) \/ (rng g))) +* (x,y)) * g) by A2, Th10, XBOOLE_1:7
.= (f +~ (x,y)) +* (g +~ (x,y)) by A1, Th118, XBOOLE_1:7 ;
:: thesis: verum