let W be Point of [:I[01],I[01]:]; :: according to BORSUK_1:def 1 :: thesis: for b₁ being a_neighborhood of (HomotopyMlt (F,G)) . W ex b₂ being a_neighborhood of W st (HomotopyMlt (F,G)) .: b₂ c= b₁
let N be a_neighborhood of (HomotopyMlt (F,G)) . W; :: thesis: ex b₁ being a_neighborhood of W st (HomotopyMlt (F,G)) .: b₁ 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