let f1, f2, g1, g2 be Function; :: thesis: ( rng g1 c= dom f1 & rng g2 c= dom f2 & f1 tolerates f2 implies (f1 +* f2) * (g1 +* g2) = (f1 * g1) +* (f2 * g2) )
assume A1: ( rng g1 c= dom f1 & rng g2 c= dom f2 & f1 tolerates f2 ) ; :: thesis: (f1 +* f2) * (g1 +* g2) = (f1 * g1) +* (f2 * g2)
then ( rng (g1 +* g2) c= (rng g1) \/ (rng g2) & dom (f1 +* f2) = (dom f1) \/ (dom f2) & (rng g1) \/ (rng g2) c= (dom f1) \/ (dom f2) ) by Def1, Th18, XBOOLE_1:13;
then A2: dom ((f1 +* f2) * (g1 +* g2)) = dom (g1 +* g2) by RELAT_1:46, XBOOLE_1:1
.= (dom g1) \/ (dom g2) by Def1 ;
A3: ( dom (f1 * g1) = dom g1 & dom (f2 * g2) = dom g2 ) by A1, RELAT_1:46;
then A4: dom ((f1 * g1) +* (f2 * g2)) = (dom g1) \/ (dom g2) by Def1;

now

let x be set ; :: thesis: ( x in (dom g1) \/ (dom g2) implies ((f1 +* f2) * (g1 +* g2)) . x = ((f1 * g1) +* (f2 * g2)) . x )
assume A5: x in (dom g1) \/ (dom g2) ; :: thesis: ((f1 +* f2) * (g1 +* g2)) . x = ((f1 * g1) +* (f2 * g2)) . x
then A6: ((f1 +* f2) * (g1 +* g2)) . x = (f1 +* f2) . ((g1 +* g2) . x) by A2, FUNCT_1:22;
( ( x in dom g1 or x in dom g2 ) & ( not x in dom g2 or x in dom g2 ) ) by A5, XBOOLE_0:def 3;
then ( ( (g1 +* g2) . x = g1 . x & ((f1 * g1) +* (f2 * g2)) . x = (f1 * g1) . x & (f1 * g1) . x = f1 . (g1 . x) & g1 . x in rng g1 & ( g1 . x in rng g1 implies g1 . x in dom f1 ) ) or ( (g1 +* g2) . x = g2 . x & ((f1 * g1) +* (f2 * g2)) . x = (f2 * g2) . x & (f2 * g2) . x = f2 . (g2 . x) & g2 . x in rng g2 & ( g2 . x in rng g2 implies g2 . x in dom f2 ) ) ) by A1, A3, A5, Def1, FUNCT_1:22, FUNCT_1:def 5;
hence ((f1 +* f2) * (g1 +* g2)) . x = ((f1 * g1) +* (f2 * g2)) . x by A1, A6, Th14, Th16; :: thesis: verum

end;

hence (f1 +* f2) * (g1 +* g2) = (f1 * g1) +* (f2 * g2) by A2, A4, FUNCT_1:9; :: thesis: verum