let f, g, h be Function; :: thesis: ( h in sproduct (f +* g) implies ex f9, g9 being Function st
( f9 in sproduct f & g9 in sproduct g & h = f9 +* g9 ) )
assume A1: h in sproduct (f +* g) ; :: thesis: ex f9, g9 being Function st
( f9 in sproduct f & g9 in sproduct g & h = f9 +* g9 )
take h | ((dom f) \ (dom g)) ; :: thesis: ex g9 being Function st
( h | ((dom f) \ (dom g)) in sproduct f & g9 in sproduct g & h = (h | ((dom f) \ (dom g))) +* g9 )
take h | (dom g) ; :: thesis: ( h | ((dom f) \ (dom g)) in sproduct f & h | (dom g) in sproduct g & h = (h | ((dom f) \ (dom g))) +* (h | (dom g)) )
A2: h | ((dom f) \ (dom g)) in sproduct ((f +* g) | ((dom f) \ (dom g))) by A1, Th66;
sproduct ((f +* g) | ((dom f) \ (dom g))) c= sproduct f by Th56, FUNCT_4:24;
hence h | ((dom f) \ (dom g)) in sproduct f by A2; :: thesis: ( h | (dom g) in sproduct g & h = (h | ((dom f) \ (dom g))) +* (h | (dom g)) )
(f +* g) | (dom g) = g ;
hence h | (dom g) in sproduct g by A1, Th66; :: thesis: h = (h | ((dom f) \ (dom g))) +* (h | (dom g))
dom h c= dom (f +* g) by A1, Th49;
then dom h c= (dom f) \/ (dom g) by FUNCT_4:def 1;
then dom h c= ((dom f) \ (dom g)) \/ (dom g) by XBOOLE_1:39;
hence h = (h | ((dom f) \ (dom g))) +* (h | (dom g)) by FUNCT_4:70; :: thesis: verum