set A = {{} };
take {{} } ; :: thesis: ( not {{} } is empty & {{} } is functional & {{} } is compatible )
{{} } 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
A1: f in {{} } and
g in {{} } ; :: thesis: f tolerates g
f = {} by A1, TARSKI:def 1;
hence f tolerates g by PARTFUN1:135, XBOOLE_1:2; :: thesis: verum
end;
hence ( not {{} } is empty & {{} } is functional & {{} } is compatible ) ; :: thesis: verum