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_{1} being Element of the carrier of I[01] holds

( (HopfHomotopy (f,g)) . (b_{1},0) = (LoopMlt (f,g)) . b_{1} & (HopfHomotopy (f,g)) . (b_{1},1) = (LoopMlt (g,f)) . b_{1} & (HopfHomotopy (f,g)) . (0,b_{1}) = t & (HopfHomotopy (f,g)) . (1,b_{1}) = t ) ) )

thus ( HopfHomotopy (f,g) is continuous & ( for b_{1} being Element of the carrier of I[01] holds

( (HopfHomotopy (f,g)) . (b_{1},0) = (LoopMlt (f,g)) . b_{1} & (HopfHomotopy (f,g)) . (b_{1},1) = (LoopMlt (g,f)) . b_{1} & (HopfHomotopy (f,g)) . (0,b_{1}) = t & (HopfHomotopy (f,g)) . (1,b_{1}) = t ) ) )
by Lm3; :: thesis: verum

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

( (HopfHomotopy (f,g)) . (b

thus ( HopfHomotopy (f,g) is continuous & ( for b

( (HopfHomotopy (f,g)) . (b