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