theorem :: RELSET_2:51

for A, B, C being set
for R being Relation of A,B
for S being Relation of B,C holds
( proj1 (R * S) = (R ~) .: (proj1 S) & proj1 (R * S) c= proj1 R )