thus LoopMlt (f,g), LoopMlt (g,f) are_homotopic by Th13; :: according to BORSUK_6:def 11 :: thesis: ( HopfHomotopy (f,g) is continuous & ( for b₁ being Element of the carrier of I[01] holds
( (HopfHomotopy (f,g)) . (b₁,0) = (LoopMlt (f,g)) . b₁ & (HopfHomotopy (f,g)) . (b₁,1) = (LoopMlt (g,f)) . b₁ & (HopfHomotopy (f,g)) . (0,b₁) = t & (HopfHomotopy (f,g)) . (1,b₁) = t ) ) )
thus ( HopfHomotopy (f,g) is continuous & ( for b₁ being Element of the carrier of I[01] holds
( (HopfHomotopy (f,g)) . (b₁,0) = (LoopMlt (f,g)) . b₁ & (HopfHomotopy (f,g)) . (b₁,1) = (LoopMlt (g,f)) . b₁ & (HopfHomotopy (f,g)) . (0,b₁) = t & (HopfHomotopy (f,g)) . (1,b₁) = t ) ) ) by Lm3; :: thesis: verum