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 :: thesis: ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h )
per cases ( Y = {} or Y <> {} ) ;
suppose A3: Y = {} ; :: thesis: ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h )
then ( f tolerates <:{},X,Y:> & g tolerates <:{},X,Y:> ) ;
hence ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h ) by A1, A3; :: thesis: verum
end;
suppose A4: Y <> {} ; :: thesis: ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h )
set y = the Element of Y;
defpred S1[ object , object ] 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 = the Element of Y ) );
A5: for x being object st x in X holds
ex y9 being object st S1[x,y9]
proof
let x be object ; :: thesis: ( x in X implies ex y9 being object st S1[x,y9] )
assume x in X ; :: thesis: ex y9 being object st S1[x,y9]
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 A6: ( x in dom f & x in dom g ) ; :: thesis: ex y9 being object st S1[x,y9]
take y9 = f . x; :: thesis: S1[x,y9]
thus ( x in dom f implies y9 = f . x ) ; :: thesis: ( ( x in dom g implies y9 = g . x ) & ( not x in dom f & not x in dom g implies y9 = the Element of Y ) )
x in (dom f) /\ (dom g) by A6, XBOOLE_0:def 4;
hence ( x in dom g implies y9 = g . x ) by A2; :: thesis: ( not x in dom f & not x in dom g implies y9 = the Element of Y )
thus ( not x in dom f & not x in dom g implies y9 = the Element of Y ) by A6; :: thesis: verum
end;
suppose A7: ( x in dom f & not x in dom g ) ; :: thesis: ex y9 being object st S1[x,y9]
take y9 = f . x; :: thesis: S1[x,y9]
thus ( ( x in dom f implies y9 = f . x ) & ( x in dom g implies y9 = g . x ) & ( not x in dom f & not x in dom g implies y9 = the Element of Y ) ) by A7; :: thesis: verum
end;
suppose A8: ( not x in dom f & x in dom g ) ; :: thesis: ex y9 being object st S1[x,y9]
take y9 = g . x; :: thesis: S1[x,y9]
thus ( ( x in dom f implies y9 = f . x ) & ( x in dom g implies y9 = g . x ) & ( not x in dom f & not x in dom g implies y9 = the Element of Y ) ) by A8; :: thesis: verum
end;
suppose ( not x in dom f & not x in dom g ) ; :: thesis: ex y9 being object st S1[x,y9]
hence ex y9 being object st S1[x,y9] ; :: thesis: verum
end;
end;
end;
A9: for x, y1, y2 being object st x in X & S1[x,y1] & S1[x,y2] holds
y1 = y2 ;
consider h being Function such that
A10: dom h = X and
A11: for x being object st x in X holds
S1[x,h . x] from FUNCT_1:sch 2(A9, A5);
 rng h c= Y
proof
let z be object ; :: 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 object such that
A12: x in dom h and
A13: z = h . x by FUNCT_1:def 3;
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 A14: ( x in dom f & x in dom g ) ; :: thesis: z in Y
then z = f . x by A11, A13;
hence z in Y by A14, Th4; :: thesis: verum
end;
suppose A15: ( x in dom f & not x in dom g ) ; :: thesis: z in Y
then z = f . x by A11, A13;
hence z in Y by A15, Th4; :: thesis: verum
end;
suppose A16: ( not x in dom f & x in dom g ) ; :: thesis: z in Y
then z = g . x by A11, A13;
hence z in Y by A16, Th4; :: thesis: verum
end;
suppose ( not x in dom f & not x in dom g ) ; :: thesis: z in Y
then z = the Element of Y by A10, A11, A12, A13;
hence z in Y by A4; :: thesis: verum
end;
end;
end;
then reconsider h9 = h as PartFunc of X,Y by A10, RELSET_1:4;
A17: f tolerates h
proof
let x be object ; :: according to PARTFUN1:def 4 :: 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 by XBOOLE_0:def 4;
hence f . x = h . x by A11; :: thesis: verum
end;
A18: g tolerates h
proof
let x be object ; :: according to PARTFUN1:def 4 :: 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 by XBOOLE_0:def 4;
hence g . x = h . x by A11; :: thesis: verum
end;
h9 is total by A10;
hence ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h ) by A17, A18; :: 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