for A, B being set
for U1, U2 being non empty set
for Q being quasi_total Relation of B,U1
for R being quasi_total Relation of B,U2
for P being Relation of A,B st ((P * Q) * (Q ~)) * R is Function-like holds
((P * Q) * (Q ~)) * R = P * R