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