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