let f, g be Function; :: thesis: for f9, g9 being Function st dom g misses (dom f9) \ (dom g9) & f9 in sproduct f & g9 in sproduct g holds
f9 +* g9 in sproduct (f +* g)
let f9, g9 be Function; :: thesis: ( dom g misses (dom f9) \ (dom g9) & f9 in sproduct f & g9 in sproduct g implies f9 +* g9 in sproduct (f +* g) )
assume that
A1: dom g misses (dom f9) \ (dom g9) and
A2: f9 in sproduct f and
A3: g9 in sproduct g ; :: thesis: f9 +* g9 in sproduct (f +* g)
set h = f9 +* g9;
A4: dom f9 c= dom f by A2, Th49;
A5: dom g9 c= dom g by A3, Th49;
then A6: (dom f9) \/ (dom g9) c= (dom f) \/ (dom g) by A4, XBOOLE_1:13;
A7: dom (f9 +* g9) = (dom f9) \/ (dom g9) by FUNCT_4:def 1;
then A8: dom (f9 +* g9) c= dom (f +* g) by A6, FUNCT_4:def 1;
for x being object st x in dom (f9 +* g9) holds
(f9 +* g9) . x in (f +* g) . x

proof

let x be object ; :: thesis: ( x in dom (f9 +* g9) implies (f9 +* g9) . x in (f +* g) . x )
assume A9: x in dom (f9 +* g9) ; :: thesis: (f9 +* g9) . x in (f +* g) . x
then x in dom (f +* g) by A8;
then A10: x in (dom f) \/ (dom g) by FUNCT_4:def 1;
x in ((dom f9) \ (dom g9)) \/ (dom g9) by A7, A9, XBOOLE_1:39;
then A11: ( x in (dom f9) \ (dom g9) or x in dom g9 ) by XBOOLE_0:def 3;

now :: thesis: ( ( x in dom g & (f9 +* g9) . x in g . x ) or ( not x in dom g & (f9 +* g9) . x in f . x ) )

per cases ( x in dom g or not x in dom g ) ;

case A12: x in dom g ; :: thesis: (f9 +* g9) . x in g . x

then (f9 +* g9) . x = g9 . x by A1, A7, A9, A11, FUNCT_4:def 1, XBOOLE_0:3;
hence (f9 +* g9) . x in g . x by A1, A3, A11, A12, Th49, XBOOLE_0:3; :: thesis: verum

end;

case not x in dom g ; :: thesis: (f9 +* g9) . x in f . x

then A13: not x in dom g9 by A5;
then A14: (f9 +* g9) . x = f9 . x by A7, A9, FUNCT_4:def 1;
x in dom f9 by A7, A9, A13, XBOOLE_0:def 3;
hence (f9 +* g9) . x in f . x by A2, A14, Th49; :: thesis: verum

end;

end;

end;

hence (f9 +* g9) . x in (f +* g) . x by A10, FUNCT_4:def 1; :: thesis: verum

end;

hence f9 +* g9 in sproduct (f +* g) by A8, Def9; :: thesis: verum