dom s c= C ;
hence dom (s *') c= C by Def1; :: according to RELAT_1:def 18 :: thesis: verum