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 )

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

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

A8:
t = 1_ T
by Def1;
let a be Point of I[01]; :: according to BORSUK_1:def 1 :: thesis: for b_{1} being a_neighborhood of (LoopMlt (f,g)) . a ex b_{2} being a_neighborhood of a st (LoopMlt (f,g)) .: b_{2} c= b_{1}

let G be a_neighborhood of (LoopMlt (f,g)) . a; :: thesis: ex b_{1} being a_neighborhood of a st (LoopMlt (f,g)) .: b_{1} 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

end;let G be a_neighborhood of (LoopMlt (f,g)) . a; :: thesis: ex b

(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

hence
(LoopMlt (f,g)) .: H c= G
by A2; :: thesis: verum
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;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

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