let W be Point of [:I[01],I[01]:]; :: according to BORSUK_1:def 1 :: thesis: for b_{1} being a_neighborhood of (HomotopyMlt (F,G)) . W ex b_{2} being a_neighborhood of W st (HomotopyMlt (F,G)) .: b_{2} c= b_{1}

let N be a_neighborhood of (HomotopyMlt (F,G)) . W; :: thesis: ex b_{1} being a_neighborhood of W st (HomotopyMlt (F,G)) .: b_{1} c= N

consider a, b being Point of I[01] such that

A1: W = [a,b] by BORSUK_1:10;

(HomotopyMlt (F,G)) . (a,b) = (F . (a,b)) * (G . (a,b)) by Def7;

then consider A being open a_neighborhood of F . (a,b), B being open a_neighborhood of G . (a,b) such that

A2: A * B c= N by A1, TOPGRP_1:37;

consider NF being a_neighborhood of [a,b] such that

A3: F .: NF c= A by BORSUK_1:def 1;

consider NG being a_neighborhood of [a,b] such that

A4: G .: NG c= B by BORSUK_1:def 1;

reconsider H = NF /\ NG as a_neighborhood of W by A1, CONNSP_2:2;

take H ; :: thesis: (HomotopyMlt (F,G)) .: H c= N

A5: (HomotopyMlt (F,G)) .: (NF /\ NG) c= (F .: NF) * (G .: NG) by Th8;

(F .: NF) * (G .: NG) c= A * B by A3, A4, TOPGRP_1:4;

hence (HomotopyMlt (F,G)) .: H c= N by A5, A2; :: thesis: verum

let N be a_neighborhood of (HomotopyMlt (F,G)) . W; :: thesis: ex b

consider a, b being Point of I[01] such that

A1: W = [a,b] by BORSUK_1:10;

(HomotopyMlt (F,G)) . (a,b) = (F . (a,b)) * (G . (a,b)) by Def7;

then consider A being open a_neighborhood of F . (a,b), B being open a_neighborhood of G . (a,b) such that

A2: A * B c= N by A1, TOPGRP_1:37;

consider NF being a_neighborhood of [a,b] such that

A3: F .: NF c= A by BORSUK_1:def 1;

consider NG being a_neighborhood of [a,b] such that

A4: G .: NG c= B by BORSUK_1:def 1;

reconsider H = NF /\ NG as a_neighborhood of W by A1, CONNSP_2:2;

take H ; :: thesis: (HomotopyMlt (F,G)) .: H c= N

A5: (HomotopyMlt (F,G)) .: (NF /\ NG) c= (F .: NF) * (G .: NG) by Th8;

(F .: NF) * (G .: NG) c= A * B by A3, A4, TOPGRP_1:4;

hence (HomotopyMlt (F,G)) .: H c= N by A5, A2; :: thesis: verum