theorem :: RELSET_2:52

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