theorem Th75: :: FUNCT_1:76

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