for X being set
for f, g being Relation of X,X st rng f = X & rng g = X holds
rng (g * f) = X