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