let a, b, c, d, e, f be object ; 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
;
verum