set F = LoopMlt (f,g);
thus A1: t,t are_connected ; :: according to BORSUK_2:def 2 :: thesis: ( LoopMlt (f,g) is continuous & (LoopMlt (f,g)) . 0 = t & (LoopMlt (f,g)) . 1 = t )
thus LoopMlt (f,g) is continuous :: thesis: ( (LoopMlt (f,g)) . 0 = t & (LoopMlt (f,g)) . 1 = t )

proof

let a be Point of I[01]; :: according to BORSUK_1:def 1 :: thesis: for b₁ being a_neighborhood of (LoopMlt (f,g)) . a ex b₂ being a_neighborhood of a st (LoopMlt (f,g)) .: b₂ c= b₁
let G be a_neighborhood of (LoopMlt (f,g)) . a; :: thesis: ex b₁ being a_neighborhood of a st (LoopMlt (f,g)) .: b₁ c= G
(LoopMlt (f,g)) . a = (f . a) * (g . a) by Def2;
then consider A being open a_neighborhood of f . a, B being open a_neighborhood of g . a such that
A2: A * B c= G by TOPGRP_1:37;
consider Ha being a_neighborhood of a such that
A3: f .: Ha c= A by BORSUK_1:def 1;
consider Hb being a_neighborhood of a such that
A4: g .: Hb c= B by BORSUK_1:def 1;
reconsider H = Ha /\ Hb as a_neighborhood of a by CONNSP_2:2;
take H ; :: thesis: (LoopMlt (f,g)) .: H c= G
(LoopMlt (f,g)) .: H c= A * B

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (LoopMlt (f,g)) .: H or y in A * B )
assume y in (LoopMlt (f,g)) .: H ; :: thesis: y in A * B
then consider c being Element of I[01] such that
A5: c in H and
A6: (LoopMlt (f,g)) . c = y by FUNCT_2:65;
A7: (LoopMlt (f,g)) . c = (f . c) * (g . c) by Def2;
( c in Ha & c in Hb ) by A5, XBOOLE_0:def 4;
then ( f . c in f .: Ha & g . c in g .: Hb ) by FUNCT_2:35;
hence y in A * B by A3, A4, A6, A7; :: thesis: verum

end;

hence (LoopMlt (f,g)) .: H c= G by A2; :: thesis: verum

end;

A8: t = 1_ T by Def1;
A9: (1_ T) * (1_ T) = 1_ T ;
( f . 0[01] = t & g . 0[01] = t & f . 1[01] = t & g . 1[01] = t ) by A1, BORSUK_2:def 2;
hence ( (LoopMlt (f,g)) . 0 = t & (LoopMlt (f,g)) . 1 = t ) by A8, A9, Def2; :: thesis: verum