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 set st x in (dom f) /\ (dom g) holds
f . x = g . x ; :: according to PARTFUN1:def 6 :: thesis: f * tolerates g *
let x be set ; :: according to PARTFUN1:def 6 :: thesis: ( not x in (proj1 (f *)) /\ (proj1 (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 14;
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

let i be set ; :: 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 5;
p . i in rng p by A7, FUNCT_1:def 5;
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:23 ;
hence (f * p) . i = (g * q) . i by A7, FUNCT_1:23; :: thesis: verum

end;

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