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 A1, Th9; :: according to BORSUK_6:def 11 :: thesis: ( HomotopyMlt (F,G) is continuous & ( for b_{1} being Element of the carrier of I[01] holds

( (HomotopyMlt (F,G)) . (b_{1},0) = (LoopMlt (f1,g1)) . b_{1} & (HomotopyMlt (F,G)) . (b_{1},1) = (LoopMlt (f2,g2)) . b_{1} & (HomotopyMlt (F,G)) . (0,b_{1}) = t & (HomotopyMlt (F,G)) . (1,b_{1}) = t ) ) )

( F is continuous & G is continuous ) by A1, BORSUK_6:def 11;

hence HomotopyMlt (F,G) is continuous ; :: thesis: for b_{1} being Element of the carrier of I[01] holds

( (HomotopyMlt (F,G)) . (b_{1},0) = (LoopMlt (f1,g1)) . b_{1} & (HomotopyMlt (F,G)) . (b_{1},1) = (LoopMlt (f2,g2)) . b_{1} & (HomotopyMlt (F,G)) . (0,b_{1}) = t & (HomotopyMlt (F,G)) . (1,b_{1}) = t )

thus for b_{1} being Element of the carrier of I[01] holds

( (HomotopyMlt (F,G)) . (b_{1},0) = (LoopMlt (f1,g1)) . b_{1} & (HomotopyMlt (F,G)) . (b_{1},1) = (LoopMlt (f2,g2)) . b_{1} & (HomotopyMlt (F,G)) . (0,b_{1}) = t & (HomotopyMlt (F,G)) . (1,b_{1}) = t )
by A1, Lm2; :: thesis: verum

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 A1, Th9; :: according to BORSUK_6:def 11 :: thesis: ( HomotopyMlt (F,G) is continuous & ( for b

( (HomotopyMlt (F,G)) . (b

( F is continuous & G is continuous ) by A1, BORSUK_6:def 11;

hence HomotopyMlt (F,G) is continuous ; :: thesis: for b

( (HomotopyMlt (F,G)) . (b

thus for b

( (HomotopyMlt (F,G)) . (b