for D, E, F being non empty set
for P being Relation of D,E
for R being Relation of E,F
for x, z being object holds
( [x,z] in P * R iff ex y being Element of E st
( [x,y] in P & [y,z] in R ) )