let a, b, c, x, y, z be object ; :: thesis: dom ((a,b,c) --> (x,y,z)) = {a,b,c}
A1: ( dom ((a,b) --> (x,y)) = {a,b} & dom (c .--> z) = {c} ) by Th62;
thus dom ((a,b,c) --> (x,y,z)) = (dom ((a,b) --> (x,y))) \/ (dom (c .--> z)) by Def1
.= {a,b,c} by A1, ENUMSET1:3 ; :: thesis: verum