let X1, Y1, X2, Y2 be non empty set ; :: thesis: for f being Function of X1,X2
for g being Function of Y1,Y2 st f tolerates g holds
f * tolerates g *
let f be Function of X1,X2; :: thesis: for g being Function of Y1,Y2 st f tolerates g holds
f * tolerates g *
let g be Function of Y1,Y2; :: thesis: ( f tolerates g implies f * tolerates g * )
A1: dom g = Y1 by FUNCT_2:def 1;
assume A2: for x being object st x in (dom f) /\ (dom g) holds
f . x = g . x ; :: according to PARTFUN1:def 4 :: thesis: f * tolerates g *
let x be object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (dom (f *)) /\ (dom (g *)) or (f *) . x = (g *) . x )
assume A3: x in (dom (f *)) /\ (dom (g *)) ; :: thesis: (f *) . x = (g *) . x
then reconsider q = x as Element of Y1 * ;
A4: (g *) . x = g * q by LANG1:def 13;
x in dom (f *) by A3, XBOOLE_0:def 4;
then reconsider p = x as Element of X1 * ;
A5: dom f = X1 by FUNCT_2:def 1;

A6: now :: thesis: for i being object st i in dom p holds
(f * p) . i = (g * q) . i

let i be object ; :: thesis: ( i in dom p implies (f * p) . i = (g * q) . i )
assume A7: i in dom p ; :: thesis: (f * p) . i = (g * q) . i
then A8: q . i in rng q by FUNCT_1:def 3;
p . i in rng p by A7, FUNCT_1:def 3;
then p . i in (dom f) /\ (dom g) by A5, A1, A8, XBOOLE_0:def 4;
then f . (p . i) = g . (q . i) by A2
.= (g * q) . i by A7, FUNCT_1:13 ;
hence (f * p) . i = (g * q) . i by A7, FUNCT_1:13; :: thesis: verum

end;

rng q c= Y1 ;
then A9: dom (g * q) = dom q by A1, RELAT_1:27;
rng p c= X1 ;
then A10: dom (f * p) = dom p by A5, RELAT_1:27;
(f *) . x = f * p by LANG1:def 13;
hence (f *) . x = (g *) . x by A4, A10, A9, A6; :: thesis: verum