let f, g, h be Function; :: thesis:
assume that
A1: g in sproduct f and
A2: h in sproduct f ; :: thesis:
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;

let x be object ; :: thesis:
assume x in dom (g +* h) ; :: thesis:
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;

per cases by A5, XBOOLE_0:def 3;

suppose A6: x in dom h ; :: thesis:

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

end;

suppose A7: x in (dom g) \ (dom h) ; :: thesis:

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:

end;

end;

end;

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

end;

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