let f1, f2, g1, g2 be Function; :: thesis: ( f1 tolerates f2 & g1 tolerates g2 implies f1 * g1 tolerates f2 * g2 )
assume that
A1: for x being set st x in (dom f1) /\ (dom f2) holds
f1 . x = f2 . x and
A2: for x being set st x in (dom g1) /\ (dom g2) holds
g1 . x = g2 . x ; :: according to PARTFUN1:def 6 :: thesis: f1 * g1 tolerates f2 * g2
let x be set ; :: according to PARTFUN1:def 6 :: thesis: ( not x in (dom (f1 * g1)) /\ (dom (f2 * g2)) or (f1 * g1) . x = (f2 * g2) . x )
assume x in (dom (f1 * g1)) /\ (dom (f2 * g2)) ; :: thesis: (f1 * g1) . x = (f2 * g2) . x
then ( x in dom (f1 * g1) & x in dom (f2 * g2) ) by XBOOLE_0:def 4;
then A3: ( x in dom g1 & g1 . x in dom f1 & x in dom g2 & g2 . x in dom f2 ) by FUNCT_1:21;
then x in (dom g1) /\ (dom g2) by XBOOLE_0:def 4;
then A4: g1 . x = g2 . x by A2;
then ( g1 . x in (dom f1) /\ (dom f2) & (f1 * g1) . x = f1 . (g1 . x) & (f2 * g2) . x = f2 . (g2 . x) ) by A3, FUNCT_1:23, XBOOLE_0:def 4;
hence (f1 * g1) . x = (f2 * g2) . x by A1, A4; :: thesis: verum