let f, g, h be Function; :: thesis: ( g in product f & h in sproduct f implies g +* h in product f )
assume A1: g in product f ; :: thesis: ( not h in sproduct f or g +* h in product f )
then A2: dom g = dom f by Th9;
assume A3: h in sproduct f ; :: thesis: g +* h in product f
then A4: (dom g) \/ (dom h) = dom f by A2, Th49, XBOOLE_1:12;
then A5: dom (g +* h) = dom f by FUNCT_4:def 1;

now :: thesis: for x being object st x in dom f holds
(g +* h) . x in f . x

let x be object ; :: thesis: ( x in dom f implies (g +* h) . x in f . x )
assume A6: x in dom f ; :: thesis: (g +* h) . x in f . x
A7: ((dom g) \ (dom h)) \/ (dom h) = dom f by A4, XBOOLE_1:39;

now :: thesis: ( ( x in (dom g) \ (dom h) & x in dom f & (g +* h) . x = g . x ) or ( x in dom h & (g +* h) . x = h . x ) )

per cases ( x in (dom g) \ (dom h) or x in dom h ) by A6, A7, XBOOLE_0:def 3;

case A8: x in (dom g) \ (dom h) ; :: thesis: ( x in dom f & (g +* h) . x = g . x )

then not x in dom h by XBOOLE_0:def 5;
hence ( x in dom f & (g +* h) . x = g . x ) by A2, A8, FUNCT_4:11; :: thesis: verum

end;

case x in dom h ; :: thesis: (g +* h) . x = h . x

hence (g +* h) . x = h . x by FUNCT_4:13; :: thesis: verum

end;

end;

end;

hence (g +* h) . x in f . x by A1, A3, Th9, Th49; :: thesis: verum

end;

hence g +* h in product f by A5, Th9; :: thesis: verum