:: deftheorem Def7 defines HomotopyMlt TOPALG_7:def 7 :
for T being non empty multMagma
for F, G, b₄ being Function of [:I[01],I[01]:],T holds
( b₄ = HomotopyMlt (F,G) iff for a, b being Point of I[01] holds b₄ . (a,b) = (F . (a,b)) * (G . (a,b)) );