set F = HopfHomotopy (f,g);
set i = inverse_loop f;
let W be Point of ; :: according to BORSUK_1:def 1 :: thesis: for b1 being a_neighborhood of (HopfHomotopy (f,g)) . W ex b2 being a_neighborhood of W st (HopfHomotopy (f,g)) .: b2 c= b1
let G be a_neighborhood of (HopfHomotopy (f,g)) . W; :: thesis: ex b1 being a_neighborhood of W st (HopfHomotopy (f,g)) .: b1 c= G
consider a, b being Point of I such that
A1: W = [a,b] by BORSUK_1:10;
(HopfHomotopy (f,g)) . (a,b) = (((() . (a * b)) * (f . a)) * (g . a)) * (f . (a * b)) by Def8;
then consider A1 being open a_neighborhood of ((() . (a * b)) * (f . a)) * (g . a), B1 being open a_neighborhood of f . (a * b) such that
A2: A1 * B1 c= G by ;
consider A2 being open a_neighborhood of (() . (a * b)) * (f . a), B2 being open a_neighborhood of g . a such that
A3: A2 * B2 c= A1 by TOPGRP_1:37;
consider A3 being open a_neighborhood of () . (a * b), B3 being open a_neighborhood of f . a such that
A4: A3 * B3 c= A2 by TOPGRP_1:37;
() . (a * b) = () . (f . (a * b)) by FUNCT_2:15
.= (f . (a * b)) " by GROUP_1:def 6 ;
then consider A4 being open a_neighborhood of f . (a * b) such that
A5: A4 " c= A3 by TOPGRP_1:39;
consider A5 being a_neighborhood of a * b such that
A6: f .: A5 c= A4 by BORSUK_1:def 1;
consider NB1 being a_neighborhood of a * b such that
A7: f .: NB1 c= B1 by BORSUK_1:def 1;
consider NB2 being a_neighborhood of a such that
A8: g .: NB2 c= B2 by BORSUK_1:def 1;
consider NB3 being a_neighborhood of a such that
A9: f .: NB3 c= B3 by BORSUK_1:def 1;
A5 /\ NB1 is a_neighborhood of a * b by CONNSP_2:2;
then consider N1 being a_neighborhood of a, N2 being a_neighborhood of b such that
A10: for x, y being Point of I st x in N1 & y in N2 holds
x * y in A5 /\ NB1 by Th7;
N1 /\ NB2 is a_neighborhood of a by CONNSP_2:2;
then reconsider Na = (N1 /\ NB2) /\ NB3 as a_neighborhood of a by CONNSP_2:2;
reconsider H = [:Na,N2:] as a_neighborhood of W by A1;
take H ; :: thesis: (HopfHomotopy (f,g)) .: H c= G
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (HopfHomotopy (f,g)) .: H or y in G )
assume y in (HopfHomotopy (f,g)) .: H ; :: thesis: y in G
then consider x being Element of such that
A11: x in H and
A12: (HopfHomotopy (f,g)) . x = y by FUNCT_2:65;
consider c, d being Point of I such that
A13: x = [c,d] by BORSUK_1:10;
A14: () . (c * d) = () . (f . (c * d)) by FUNCT_2:15
.= (f . (c * d)) " by GROUP_1:def 6 ;
A15: (HopfHomotopy (f,g)) . (c,d) = (((() . (c * d)) * (f . c)) * (g . c)) * (f . (c * d)) by Def8;
A16: c in (N1 /\ NB2) /\ NB3 by ;
A17: c in N1 /\ NB2 by ;
then A18: c in N1 by XBOOLE_0:def 4;
d in N2 by ;
then A19: c * d in A5 /\ NB1 by ;
then c * d in A5 by XBOOLE_0:def 4;
then f . (c * d) in f .: A5 by FUNCT_2:35;
then A20: (f . (c * d)) " in A4 " by A6;
c in NB3 by ;
then f . c in f .: NB3 by FUNCT_2:35;
then A21: ((inverse_loop f) . (c * d)) * (f . c) in A3 * B3 by A5, A9, A14, A20;
c in NB2 by ;
then g . c in g .: NB2 by FUNCT_2:35;
then A22: (((inverse_loop f) . (c * d)) * (f . c)) * (g . c) in A2 * B2 by A4, A8, A21;
c * d in NB1 by ;
then f . (c * d) in f .: NB1 by FUNCT_2:35;
then ((((inverse_loop f) . (c * d)) * (f . c)) * (g . c)) * (f . (c * d)) in A1 * B1 by A3, A7, A22;
hence y in G by A2, A12, A13, A15; :: thesis: verum