theorem FlipCompose: :: ROUGHS_5:5

for R being non empty RelStr
for f, g being map of R holds Flip (f * g) = (Flip f) * (Flip g)