let A, B be set ; :: thesis: field ({} A,B) = {}
(dom ({} A,B)) \/ (rng ({} A,B)) = rng ({} A,B) by RELAT_1:60;
hence field ({} A,B) = {} by RELAT_1:def 6; :: thesis: verum