let x, y, w, z, a, b, c, d be set ; :: thesis: dom (x,y,w,z --> a,b,c,d) = {x,y,w,z}
set f = x,y --> a,b;
set g = w,z --> c,d;
A1: dom (x,y --> a,b) = {x,y} by FUNCT_4:65;
dom (w,z --> c,d) = {w,z} by FUNCT_4:65;
then (dom (x,y --> a,b)) \/ (dom (w,z --> c,d)) = {x,y,w,z} by A1, ENUMSET1:45;
hence dom (x,y,w,z --> a,b,c,d) = {x,y,w,z} by FUNCT_4:def 1; :: thesis: verum