let g, f be Function; :: thesis: for f', g' being Function st dom f' misses (dom g) \ (dom g') & f' in sproduct f & g' in sproduct g holds
f' +* g' in sproduct (f +* g)
let f', g' be Function; :: thesis: ( dom f' misses (dom g) \ (dom g') & f' in sproduct f & g' in sproduct g implies f' +* g' in sproduct (f +* g) )
assume dom f' misses (dom g) \ (dom g') ; :: thesis: ( not f' in sproduct f or not g' in sproduct g or f' +* g' in sproduct (f +* g) )
then dom g misses (dom f') \ (dom g') by XBOOLE_1:81;
hence ( not f' in sproduct f or not g' in sproduct g or f' +* g' in sproduct (f +* g) ) by Th84; :: thesis: verum