set A = {{} };

now

let x be Element of {{} }; :: thesis: x is PartFunc of X,Y
A1: x = {} by TARSKI:def 1;
( dom {} c= X & rng {} c= Y ) by XBOOLE_1:2;
hence x is PartFunc of X,Y by A1, RELSET_1:11; :: thesis: verum

end;

then A2: {{} } is PFUNC_DOMAIN of X,Y by RFUNCT_3:def 3;
{{} } is compatible

proof

let f, g be Function; :: according to COMPUT_1:def 1 :: thesis: ( f in {{} } & g in {{} } implies f tolerates g )
assume ( f in {{} } & g in {{} } ) ; :: thesis: f tolerates g
then f = {} by TARSKI:def 1;
hence f tolerates g by PARTFUN1:135, XBOOLE_1:2; :: thesis: verum

end;

hence ex b₁ being PFUNC_DOMAIN of X,Y st
( not b₁ is empty & b₁ is compatible ) by A2; :: thesis: verum