let R be Relation of X,Y; :: thesis: R is total
thus dom R = X ; :: according to PARTFUN1:def 2 :: thesis: verum