set F = HopfHomotopy (f,g);

set i = inverse_loop f;

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

let G be a_neighborhood of (HopfHomotopy (f,g)) . W; :: thesis: ex b_{1} being a_neighborhood of W st (HopfHomotopy (f,g)) .: b_{1} 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 ; :: 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 [: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; :: thesis: verum

set i = inverse_loop f;

let W be Point of [:I[01],I[01]:]; :: according to BORSUK_1:def 1 :: thesis: for b

let G be a_neighborhood of (HopfHomotopy (f,g)) . W; :: thesis: ex b

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 ; :: 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 [: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; :: thesis: verum