:: deftheorem defines inverse_loop TOPALG_7:def 4 :
for T being TopGroup
for t being Point of T
for f being Loop of t holds inverse_loop f = (inverse_op T) * f;