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

now

let x be set ; :: 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 A3: x in ((dom g) \ (dom h)) \/ (dom h) by XBOOLE_1:39;

now

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

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

then h . x in f . x by A1, Th65;
hence (g +* h) . x in f . x by A4, FUNCT_4:14; :: thesis: verum

end;

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

then A6: g . x in f . x by A1, Th65;
not x in dom h by A5, XBOOLE_0:def 5;
hence (g +* h) . x in f . x by A6, FUNCT_4:12; :: thesis: verum

end;

end;

end;

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

end;

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