( dom R c= A & dom (R * S) c= dom R ) by Def18, Th44;
hence dom (R * S) c= A by XBOOLE_1:1; :: according to RELAT_1:def 18 :: thesis: verum