let W be Point of ; :: according to BORSUK_1:def 1 :: thesis: for b1 being a_neighborhood of (HomotopyMlt (F,G)) . W ex b2 being a_neighborhood of W st (HomotopyMlt (F,G)) .: b2 c= b1
let N be a_neighborhood of (HomotopyMlt (F,G)) . W; :: thesis: ex b1 being a_neighborhood of W st (HomotopyMlt (F,G)) .: b1 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 ;
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 ;
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 ;
hence (HomotopyMlt (F,G)) .: H c= N by A5, A2; :: thesis: verum