let X, Y be set ; :: thesis: for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds
ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h )
let f, g be PartFunc of X,Y; :: thesis: ( ( Y = {} implies X = {} ) & f tolerates g implies ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h ) )
assume that
A1: ( Y = {} implies X = {} ) and
A2: f tolerates g ; :: thesis: ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h )

now

per cases ( Y = {} or Y <> {} ) ;

suppose Y = {} ; :: thesis: ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h )

then ( <:{} ,X,Y:> is total & f tolerates <:{} ,X,Y:> & g tolerates <:{} ,X,Y:> ) by A1;
hence ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h ) ; :: thesis: verum

end;

suppose A3: Y <> {} ; :: thesis: ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h )

consider y being Element of Y;
defpred S₁[ set , set ] means ( ( $1 in dom f implies $2 = f . $1 ) & ( $1 in dom g implies $2 = g . $1 ) & ( not $1 in dom f & not $1 in dom g implies $2 = y ) );
A4: for x being set st x in X holds
ex y' being set st S₁[x,y']

proof

let x be set ; :: thesis: ( x in X implies ex y' being set st S₁[x,y'] )
assume x in X ; :: thesis: ex y' being set st S₁[x,y']

now

per cases ( ( x in dom f & x in dom g ) or ( x in dom f & not x in dom g ) or ( not x in dom f & x in dom g ) or ( not x in dom f & not x in dom g ) ) ;

suppose A5: ( x in dom f & x in dom g ) ; :: thesis: ex y' being set st
( ( x in dom f implies y' = f . x ) & ( x in dom g implies y' = g . x ) & ( not x in dom f & not x in dom g implies y' = y ) )

take y' = f . x; :: thesis: ( ( x in dom f implies y' = f . x ) & ( x in dom g implies y' = g . x ) & ( not x in dom f & not x in dom g implies y' = y ) )
thus ( x in dom f implies y' = f . x ) ; :: thesis: ( ( x in dom g implies y' = g . x ) & ( not x in dom f & not x in dom g implies y' = y ) )
x in (dom f) /\ (dom g) by A5, XBOOLE_0:def 4;
hence ( x in dom g implies y' = g . x ) by A2, Def6; :: thesis: ( not x in dom f & not x in dom g implies y' = y )
thus ( not x in dom f & not x in dom g implies y' = y ) by A5; :: thesis: verum

end;

suppose A6: ( x in dom f & not x in dom g ) ; :: thesis: ex y' being set st
( ( x in dom f implies y' = f . x ) & ( x in dom g implies y' = g . x ) & ( not x in dom f & not x in dom g implies y' = y ) )

take y' = f . x; :: thesis: ( ( x in dom f implies y' = f . x ) & ( x in dom g implies y' = g . x ) & ( not x in dom f & not x in dom g implies y' = y ) )
thus ( ( x in dom f implies y' = f . x ) & ( x in dom g implies y' = g . x ) & ( not x in dom f & not x in dom g implies y' = y ) ) by A6; :: thesis: verum

end;

suppose A7: ( not x in dom f & x in dom g ) ; :: thesis: ex y' being set st
( ( x in dom f implies y' = f . x ) & ( x in dom g implies y' = g . x ) & ( not x in dom f & not x in dom g implies y' = y ) )

take y' = g . x; :: thesis: ( ( x in dom f implies y' = f . x ) & ( x in dom g implies y' = g . x ) & ( not x in dom f & not x in dom g implies y' = y ) )
thus ( ( x in dom f implies y' = f . x ) & ( x in dom g implies y' = g . x ) & ( not x in dom f & not x in dom g implies y' = y ) ) by A7; :: thesis: verum

end;

suppose ( not x in dom f & not x in dom g ) ; :: thesis: ex y' being set st S₁[x,y']

hence ex y' being set st S₁[x,y'] ; :: thesis: verum

end;

end;

end;

hence ex y' being set st S₁[x,y'] ; :: thesis: verum

end;

A8: for x, y1, y2 being set st x in X & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;
consider h being Function such that
A9: dom h = X and
A10: for x being set st x in X holds
S₁[x,h . x] from FUNCT_1:sch 2(A8, A4);
A11: f tolerates h

proof

let x be set ; :: according to PARTFUN1:def 6 :: thesis: ( x in (dom f) /\ (dom h) implies f . x = h . x )
assume x in (dom f) /\ (dom h) ; :: thesis: f . x = h . x
then ( x in dom f & x in dom h ) by XBOOLE_0:def 4;
hence f . x = h . x by A10; :: thesis: verum

end;

A12: g tolerates h

proof

let x be set ; :: according to PARTFUN1:def 6 :: thesis: ( x in (dom g) /\ (dom h) implies g . x = h . x )
assume x in (dom g) /\ (dom h) ; :: thesis: g . x = h . x
then ( x in dom g & x in dom h ) by XBOOLE_0:def 4;
hence g . x = h . x by A10; :: thesis: verum

end;

rng h c= Y

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng h or z in Y )
assume z in rng h ; :: thesis: z in Y
then consider x being set such that
A13: x in dom h and
A14: z = h . x by FUNCT_1:def 5;

per cases ( ( x in dom f & x in dom g ) or ( x in dom f & not x in dom g ) or ( not x in dom f & x in dom g ) or ( not x in dom f & not x in dom g ) ) ;

suppose A15: ( x in dom f & x in dom g ) ; :: thesis: z in Y

then z = f . x by A10, A14;
hence z in Y by A15, Th27; :: thesis: verum

end;

suppose A16: ( x in dom f & not x in dom g ) ; :: thesis: z in Y

then z = f . x by A10, A14;
hence z in Y by A16, Th27; :: thesis: verum

end;

suppose A17: ( not x in dom f & x in dom g ) ; :: thesis: z in Y

then z = g . x by A10, A14;
hence z in Y by A17, Th27; :: thesis: verum

end;

suppose ( not x in dom f & not x in dom g ) ; :: thesis: z in Y

then z = y by A9, A10, A13, A14;
hence z in Y by A3; :: thesis: verum

end;

end;

end;

then reconsider h' = h as PartFunc of X,Y by A9, RELSET_1:11;
h' is total by A9, Def4;
hence ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h ) by A11, A12; :: thesis: verum

end;

end;

end;

hence ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h ) ; :: thesis: verum