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 that
A1: ( rng g1 c= dom f1 & rng g2 c= dom f2 ) and
A2: f1 tolerates f2 ; :: thesis: (f1 +* f2) * (g1 +* g2) = (f1 * g1) +* (f2 * g2)
A3: ( rng (g1 +* g2) c= (rng g1) \/ (rng g2) & dom (f1 +* f2) = (dom f1) \/ (dom f2) ) by Def1, Th17;
(rng g1) \/ (rng g2) c= (dom f1) \/ (dom f2) by A1, XBOOLE_1:13;
then A4: dom ((f1 +* f2) * (g1 +* g2)) = dom (g1 +* g2) by A3, RELAT_1:27, XBOOLE_1:1
.= (dom g1) \/ (dom g2) by Def1 ;
A5: ( dom (f1 * g1) = dom g1 & dom (f2 * g2) = dom g2 ) by A1, RELAT_1:27;
A6: now :: thesis: for x being object st x in (dom g1) \/ (dom g2) holds
((f1 +* f2) * (g1 +* g2)) . x = ((f1 * g1) +* (f2 * g2)) . x
let x be object ; :: thesis: ( x in (dom g1) \/ (dom g2) implies ((f1 +* f2) * (g1 +* g2)) . x = ((f1 * g1) +* (f2 * g2)) . x )
A7: ( not x in dom g2 or x in dom g2 ) ;
assume A8: x in (dom g1) \/ (dom g2) ; :: thesis: ((f1 +* f2) * (g1 +* g2)) . x = ((f1 * g1) +* (f2 * g2)) . x
then A9: ((f1 +* f2) * (g1 +* g2)) . x = (f1 +* f2) . ((g1 +* g2) . x) by A4, FUNCT_1:12;
( x in dom g1 or x in dom g2 ) by A8, 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, A5, A8, A7, Def1, FUNCT_1:12, FUNCT_1:def 3;
hence ((f1 +* f2) * (g1 +* g2)) . x = ((f1 * g1) +* (f2 * g2)) . x by A2, A9, Th13, Th15; :: thesis: verum
end;
dom ((f1 * g1) +* (f2 * g2)) = (dom g1) \/ (dom g2) by A5, Def1;
hence (f1 +* f2) * (g1 +* g2) = (f1 * g1) +* (f2 * g2) by A4, A6; :: thesis: verum