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₁ being Element of the carrier of I[01] holds
( (HomotopyMlt (F,G)) . (b₁,0) = (LoopMlt (f1,g1)) . b₁ & (HomotopyMlt (F,G)) . (b₁,1) = (LoopMlt (f2,g2)) . b₁ & (HomotopyMlt (F,G)) . (0,b₁) = t & (HomotopyMlt (F,G)) . (1,b₁) = t ) ) )
( F is continuous & G is continuous ) by A1, BORSUK_6:def 11;
hence HomotopyMlt (F,G) is continuous ; :: thesis: for b₁ being Element of the carrier of I[01] holds
( (HomotopyMlt (F,G)) . (b₁,0) = (LoopMlt (f1,g1)) . b₁ & (HomotopyMlt (F,G)) . (b₁,1) = (LoopMlt (f2,g2)) . b₁ & (HomotopyMlt (F,G)) . (0,b₁) = t & (HomotopyMlt (F,G)) . (1,b₁) = t )
thus for b₁ being Element of the carrier of I[01] holds
( (HomotopyMlt (F,G)) . (b₁,0) = (LoopMlt (f1,g1)) . b₁ & (HomotopyMlt (F,G)) . (b₁,1) = (LoopMlt (f2,g2)) . b₁ & (HomotopyMlt (F,G)) . (0,b₁) = t & (HomotopyMlt (F,G)) . (1,b₁) = t ) by A1, Lm2; :: thesis: verum