:: deftheorem defines LoopMlt TOPALG_7:def 3 :
for T being non empty TopGrStr
for t being Point of T
for f, g being Loop of t holds LoopMlt (f,g) = f (#) g;