theorem :: FUNCT_1:90

for X being set
for R, S being Relation st rng R c= dom S holds
R " X c= (R * S) " (S .: X)