let T be non empty TopSpace-like unital BinContinuous TopGrStr ; :: thesis: for t being unital Point of T
for f1, f2, g1, g2 being Loop of t
for F being Homotopy of f1,f2
for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds
HomotopyMlt (F,G) is Homotopy of LoopMlt (f1,g1), LoopMlt (f2,g2)

let t be unital Point of T; :: thesis: for f1, f2, g1, g2 being Loop of t
for F being Homotopy of f1,f2
for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds
HomotopyMlt (F,G) is Homotopy of LoopMlt (f1,g1), LoopMlt (f2,g2)

let f1, f2, g1, g2 be Loop of t; :: thesis: for F being Homotopy of f1,f2
for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds
HomotopyMlt (F,G) is Homotopy of LoopMlt (f1,g1), LoopMlt (f2,g2)

let F be Homotopy of f1,f2; :: thesis: for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds
HomotopyMlt (F,G) is Homotopy of LoopMlt (f1,g1), LoopMlt (f2,g2)

let G be Homotopy of g1,g2; :: thesis: ( f1,f2 are_homotopic & g1,g2 are_homotopic implies HomotopyMlt (F,G) is Homotopy of LoopMlt (f1,g1), LoopMlt (f2,g2) )
assume A1: ( f1,f2 are_homotopic & g1,g2 are_homotopic ) ; :: thesis: HomotopyMlt (F,G) is Homotopy of LoopMlt (f1,g1), LoopMlt (f2,g2)
thus LoopMlt (f1,g1), LoopMlt (f2,g2) are_homotopic by ; :: according to BORSUK_6:def 11 :: thesis: ( HomotopyMlt (F,G) is continuous & ( for b1 being Element of the carrier of I holds
( (HomotopyMlt (F,G)) . (b1,0) = (LoopMlt (f1,g1)) . b1 & (HomotopyMlt (F,G)) . (b1,1) = (LoopMlt (f2,g2)) . b1 & (HomotopyMlt (F,G)) . (0,b1) = t & (HomotopyMlt (F,G)) . (1,b1) = t ) ) )

( F is continuous & G is continuous ) by ;
hence HomotopyMlt (F,G) is continuous ; :: thesis: for b1 being Element of the carrier of I holds
( (HomotopyMlt (F,G)) . (b1,0) = (LoopMlt (f1,g1)) . b1 & (HomotopyMlt (F,G)) . (b1,1) = (LoopMlt (f2,g2)) . b1 & (HomotopyMlt (F,G)) . (0,b1) = t & (HomotopyMlt (F,G)) . (1,b1) = t )

thus for b1 being Element of the carrier of I holds
( (HomotopyMlt (F,G)) . (b1,0) = (LoopMlt (f1,g1)) . b1 & (HomotopyMlt (F,G)) . (b1,1) = (LoopMlt (f2,g2)) . b1 & (HomotopyMlt (F,G)) . (0,b1) = t & (HomotopyMlt (F,G)) . (1,b1) = t ) by ; :: thesis: verum