let f, g, h be Function; :: thesis: ( g in sproduct f & h in sproduct f implies g +* h in sproduct f )
assume that
A1: g in sproduct f and
A2: h in sproduct f ; :: thesis: g +* h in sproduct f
A3: dom g c= dom f by A1, Th49;
dom h c= dom f by A2, Th49;
then (dom g) \/ (dom h) c= dom f by A3, XBOOLE_1:8;
then A4: dom (g +* h) c= dom f by FUNCT_4:def 1;

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

let x be object ; :: thesis: ( x in dom (g +* h) implies (g +* h) . x in f . x )
assume x in dom (g +* h) ; :: thesis: (g +* h) . x in f . x
then x in (dom g) \/ (dom h) by FUNCT_4:def 1;
then A5: x in ((dom g) \ (dom h)) \/ (dom h) by XBOOLE_1:39;

now :: thesis: (g +* h) . x in f . x

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

suppose A6: x in dom h ; :: thesis: (g +* h) . x in f . x

then h . x in f . x by A2, Th49;
hence (g +* h) . x in f . x by A6, FUNCT_4:13; :: thesis: verum

end;

suppose A7: x in (dom g) \ (dom h) ; :: thesis: (g +* h) . x in f . x

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

end;

end;

end;

hence (g +* h) . x in f . x ; :: thesis: verum

end;

hence g +* h in sproduct f by A4, Def9; :: thesis: verum