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 ,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 ,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 b1 being Element of the carrier of I[01] 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 Homotopy of f1,f2 & G is Homotopy of g1,g2 ) by ;
hence ( HomotopyMlt (F,G) is continuous & ( for b1 being Element of the carrier of I[01] 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 A1, A2, A3, A4, Lm2; :: thesis: verum