:: deftheorem Def8 defines HopfHomotopy TOPALG_7:def 8 :
for T being TopGroup
for t being Point of T
for f, g being Loop of t
for b₅ being Function of [:I[01],I[01]:],T holds
( b₅ = HopfHomotopy (f,g) iff for a, b being Point of I[01] holds b₅ . (a,b) = ((((inverse_loop f) . (a * b)) * (f . a)) * (g . a)) * (f . (a * b)) );