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 st f1,f2 are_homotopic & g1,g2 are_homotopic holds
LoopMlt (f1,g1), LoopMlt (f2,g2) are_homotopic
let t be unital Point of T; :: thesis: for f1, f2, g1, g2 being Loop of t st f1,f2 are_homotopic & g1,g2 are_homotopic holds
LoopMlt (f1,g1), LoopMlt (f2,g2) are_homotopic
let f1, f2, g1, g2 be Loop of t; :: thesis: ( f1,f2 are_homotopic & g1,g2 are_homotopic implies LoopMlt (f1,g1), LoopMlt (f2,g2) are_homotopic )
assume A1: f1,f2 are_homotopic ; :: thesis: ( not g1,g2 are_homotopic or LoopMlt (f1,g1), LoopMlt (f2,g2) are_homotopic )
then consider F being Function of [:I[01],I[01]:],T such that
A2: ( F is continuous & ( for x being Point of I[01] holds
( F . (x,0) = f1 . x & F . (x,1) = f2 . x & F . (0,x) = t & F . (1,x) = t ) ) ) ;
assume A3: g1,g2 are_homotopic ; :: thesis: LoopMlt (f1,g1), LoopMlt (f2,g2) are_homotopic
then consider G being Function of [:I[01],I[01]:],T such that
A4: ( G is continuous & ( for x being Point of I[01] holds
( G . (x,0) = g1 . x & G . (x,1) = g2 . x & G . (0,x) = t & G . (1,x) = t ) ) ) ;
take HomotopyMlt (F,G) ; :: according to BORSUK_2:def 7 :: 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 Homotopy of f1,f2 & G is Homotopy of g1,g2 ) by A2, A4, A1, A3, BORSUK_6:def 11;
hence ( 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 ) ) ) by A1, A2, A3, A4, Lm2; :: thesis: verum