let T be TopologicalGroup; :: thesis: for t being unital Point of T
for f, g being Loop of t holds LoopMlt (f,g), LoopMlt (g,f) are_homotopic
let t be unital Point of T; :: thesis: for f, g being Loop of t holds LoopMlt (f,g), LoopMlt (g,f) are_homotopic
let f, g be Loop of t; :: thesis: LoopMlt (f,g), LoopMlt (g,f) are_homotopic
take HopfHomotopy (f,g) ; :: according to BORSUK_2:def 7 :: 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