let x be Element of X; :: thesis: x is total
DOM X = dom x by CARD_3:def 11;
hence x is total by PARTFUN1:def 2; :: thesis: verum