for x being Point of I[01]
for T being TopGroup
for t being Point of T
for f being Loop of t holds (inverse_loop f) . x = (f . x) "