theorem :: TOPALG_7:4

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