set A = {{}};
A1: {{}} is compatible
proof
let f, g be Function; :: according to COMPUT_1:def 1 :: thesis: ( f in {{}} & g in {{}} implies f tolerates g )
assume that
A2: f in {{}} and
g in {{}} ; :: thesis: f tolerates g
f = {} by A2, TARSKI:def 1;
hence f tolerates g ; :: thesis: verum
end;
now :: thesis: for x being Element of {{}} holds x is PartFunc of X,Y
let x be Element of {{}}; :: thesis: x is PartFunc of X,Y
x = {} by TARSKI:def 1;
hence x is PartFunc of X,Y by XBOOLE_1:2; :: thesis: verum
end;
then {{}} is PFUNC_DOMAIN of X,Y by RFUNCT_3:def 3;
hence ex b1 being PFUNC_DOMAIN of X,Y st
( not b1 is empty & b1 is compatible ) by A1; :: thesis: verum