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_{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 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_{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, A2, A3, A4, Lm2; :: thesis: verum

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

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

( 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

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