A1: dom (id X) = X by RELAT_1:45;
reconsider a = x, b = y as Element of dom (id X) by RELAT_1:45;
Swap ((id X),a,b) is onto ;
hence Swap ((id X),x,y) is onto ; :: thesis: Swap ((id X),x,y) is total
thus dom (Swap ((id X),x,y)) = X by A1, FUNCT_7:99; :: according to PARTFUN1:def 2 :: thesis: verum