( dom (X |` R) c= dom R & dom R c= A ) by Def16, Th80, XTUPLE_0:8;
hence dom (X |` R) c= A ; :: according to RELAT_1:def 18 :: thesis: verum