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