let a, b, c, d, e, f be object ; :: thesis: dom {[a,b],[c,d],[e,f]} = {a,c,e}
A1: dom {[a,b],[c,d]} = {a,c} by RELAT_1:10;
A2: dom {[e,f]} = {e} by RELAT_1:9;
{[a,b],[c,d],[e,f]} = {[a,b],[c,d]} \/ {[e,f]} by ENUMSET1:3;
hence dom {[a,b],[c,d],[e,f]} = (dom {[a,b],[c,d]}) \/ (dom {[e,f]}) by XTUPLE_0:23
.= {a,c,e} by A1, A2, ENUMSET1:3 ;
:: thesis: verum