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_{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

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

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

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