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 object st x in (dom f1) /\ (dom f2) holds
f1 . x = f2 . x and
A2: for x being object st x in (dom g1) /\ (dom g2) holds
g1 . x = g2 . x ; :: according to PARTFUN1:def 4 :: thesis: f1 * g1 tolerates f2 * g2
let x be object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (dom (f1 * g1)) /\ (dom (f2 * g2)) or (f1 * g1) . x = (f2 * g2) . x )
assume A3: x in (dom (f1 * g1)) /\ (dom (f2 * g2)) ; :: thesis: (f1 * g1) . x = (f2 * g2) . x
then A4: x in dom (f1 * g1) by XBOOLE_0:def 4;
then A5: x in dom g1 by FUNCT_1:11;
then A6: (f1 * g1) . x = f1 . (g1 . x) by FUNCT_1:13;
A7: x in dom (f2 * g2) by A3, XBOOLE_0:def 4;
then A8: x in dom g2 by FUNCT_1:11;
then A9: (f2 * g2) . x = f2 . (g2 . x) by FUNCT_1:13;
x in (dom g1) /\ (dom g2) by A5, A8, XBOOLE_0:def 4;
then A10: g1 . x = g2 . x by A2;
A11: g2 . x in dom f2 by A7, FUNCT_1:11;
g1 . x in dom f1 by A4, FUNCT_1:11;
then g1 . x in (dom f1) /\ (dom f2) by A11, A10, XBOOLE_0:def 4;
hence (f1 * g1) . x = (f2 * g2) . x by A1, A10, A6, A9; :: thesis: verum