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

proof

let x be set ; :: thesis: ( x in dom (f' +* g') implies (f' +* g') . x in (f +* g) . x )
assume A9: x in dom (f' +* g') ; :: thesis: (f' +* g') . 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 f') \ (dom g')) \/ (dom g') by A7, A9, XBOOLE_1:39;
then A11: ( x in (dom f') \ (dom g') or x in dom g' ) by XBOOLE_0:def 3;

now

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

case A12: x in dom g ; :: thesis: (f' +* g') . x in g . x

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

end;

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

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

end;

end;

end;

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

end;

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