set F = HopfHomotopy (f,g);
set i = inverse_loop f;
let W be Point of [:I[01],I[01]:]; BORSUK_1:def 1 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; ex b1 being a_neighborhood of W st (HopfHomotopy (f,g)) .: b1 c= G
consider a, b being Point of I[01] such that
A1:
W = [a,b]
by BORSUK_1:10;
(HopfHomotopy (f,g)) . (a,b) = ((((inverse_loop f) . (a * b)) * (f . a)) * (g . a)) * (f . (a * b))
by Def8;
then consider A1 being open a_neighborhood of (((inverse_loop f) . (a * b)) * (f . a)) * (g . a), B1 being open a_neighborhood of f . (a * b) such that
A2:
A1 * B1 c= G
by A1, TOPGRP_1:37;
consider A2 being open a_neighborhood of ((inverse_loop f) . (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 (inverse_loop f) . (a * b), B3 being open a_neighborhood of f . a such that
A4:
A3 * B3 c= A2
by TOPGRP_1:37;
(inverse_loop f) . (a * b) =
(inverse_op T) . (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[01] 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
; (HopfHomotopy (f,g)) .: H c= G
let y be object ; TARSKI:def 3 ( not y in (HopfHomotopy (f,g)) .: H or y in G )
assume
y in (HopfHomotopy (f,g)) .: H
; y in G
then consider x being Element of [:I[01],I[01]:] such that
A11:
x in H
and
A12:
(HopfHomotopy (f,g)) . x = y
by FUNCT_2:65;
consider c, d being Point of I[01] such that
A13:
x = [c,d]
by BORSUK_1:10;
A14: (inverse_loop f) . (c * d) =
(inverse_op T) . (f . (c * d))
by FUNCT_2:15
.=
(f . (c * d)) "
by GROUP_1:def 6
;
A15:
(HopfHomotopy (f,g)) . (c,d) = ((((inverse_loop f) . (c * d)) * (f . c)) * (g . c)) * (f . (c * d))
by Def8;
A16:
c in (N1 /\ NB2) /\ NB3
by A11, A13, ZFMISC_1:87;
A17:
c in N1 /\ NB2
by A16, XBOOLE_0:def 4;
then A18:
c in N1
by XBOOLE_0:def 4;
d in N2
by A11, A13, ZFMISC_1:87;
then A19:
c * d in A5 /\ NB1
by A18, A10;
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 A16, XBOOLE_0:def 4;
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 A17, XBOOLE_0:def 4;
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 A19, XBOOLE_0:def 4;
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; verum