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);
C: g +~ x,y = ((id ((rng f) \/ (rng g))) +* x,y) * g by Th118, XBOOLE_1:7;
B: dom ((id ((rng f) \/ (rng g))) +* x,y) = dom (id ((rng f) \/ (rng g))) by Th32
.= (rng f) \/ (rng g) by RELAT_1:71 ;
rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:18;
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 B, Th10, XBOOLE_1:7
.= (f +~ x,y) +* (g +~ x,y) by Th118, C, XBOOLE_1:7 ;
:: thesis: verum