A1: dom (id X) = X ;
reconsider a = x, b = y as Element of dom (id X) ;
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