dom (x .--> y) = {x} by Th19;
hence dom (x .--> y) c= A by ZFMISC_1:37; :: according to RELAT_1:def 18 :: thesis: verum