theorem Th3: :: TOPALG_7:3

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) = 1_ T