let P, Q be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1 being Point of (TOP-REAL 2)

for f being Function of I[01],((TOP-REAL 2) | P)

for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 1 >= t & t > s1 holds

not f . t in Q ) holds

for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q

let p1, p2, q1 be Point of (TOP-REAL 2); :: thesis: for f being Function of I[01],((TOP-REAL 2) | P)

for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 1 >= t & t > s1 holds

not f . t in Q ) holds

for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q

let f be Function of I[01],((TOP-REAL 2) | P); :: thesis: for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 1 >= t & t > s1 holds

not f . t in Q ) holds

for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q

let s1 be Real; :: thesis: ( q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 1 >= t & t > s1 holds

not f . t in Q ) implies for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q )

assume that

A1: q1 in P and

A2: f . s1 = q1 and

A3: f is being_homeomorphism and

A4: f . 0 = p1 and

A5: f . 1 = p2 and

A6: ( 0 <= s1 & s1 <= 1 ) and

A7: for t being Real st 1 >= t & t > s1 holds

not f . t in Q ; :: thesis: for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q

reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1;

let g be Function of I[01],((TOP-REAL 2) | P); :: thesis: for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q

let s2 be Real; :: thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 implies for t being Real st 1 >= t & t > s2 holds

not g . t in Q )

assume that

A8: g is being_homeomorphism and

A9: g . 0 = p1 and

A10: g . 1 = p2 and

A11: g . s2 = q1 and

A12: 0 <= s2 and

A13: s2 <= 1 ; :: thesis: for t being Real st 1 >= t & t > s2 holds

not g . t in Q

reconsider f = f, g = g as Function of I[01],((TOP-REAL 2) | P9) ;

A14: f is one-to-one by A3, TOPS_2:def 5;

set fg = (f ") * g;

let t be Real; :: thesis: ( 1 >= t & t > s2 implies not g . t in Q )

assume that

A15: 1 >= t and

A16: t > s2 ; :: thesis: not g . t in Q

reconsider t1 = t, s29 = s2 as Point of I[01] by A12, A13, A15, A16, BORSUK_1:43;

A17: t in the carrier of I[01] by A12, A15, A16, BORSUK_1:43;

reconsider Ft = ((f ") * g) . t1 as Real by BORSUK_1:40;

A18: rng g = [#] ((TOP-REAL 2) | P) by A8, TOPS_2:def 5;

A19: f " is being_homeomorphism by A3, TOPS_2:56;

then (f ") * g is being_homeomorphism by A8, TOPS_2:57;

then A20: ( (f ") * g is continuous & (f ") * g is one-to-one ) by TOPS_2:def 5;

A21: dom f = [#] I[01] by A3, TOPS_2:def 5;

then A22: 0 in dom f by BORSUK_1:43;

A23: rng f = [#] ((TOP-REAL 2) | P) by A3, TOPS_2:def 5;

then f is onto by FUNCT_2:def 3;

then A24: f " = f " by A14, TOPS_2:def 4;

then A25: (f ") . p1 = 0 by A4, A22, A14, FUNCT_1:32;

A26: 1 in dom f by A21, BORSUK_1:43;

A27: (f ") . p2 = 1 by A24, A5, A26, A14, FUNCT_1:32;

A28: dom g = [#] I[01] by A8, TOPS_2:def 5;

then 0 in dom g by BORSUK_1:43;

then A29: ((f ") * g) . 0 = 0 by A9, A25, FUNCT_1:13;

1 in dom g by A28, BORSUK_1:43;

then A30: ((f ") * g) . 1 = 1 by A10, A27, FUNCT_1:13;

A31: Ft <= 1

then A32: t in dom ((f ") * g) by A28, A18, A17, RELAT_1:27;

f * ((f ") * g) = g * (f * (f ")) by RELAT_1:36

.= g * (id (rng f)) by A23, A14, TOPS_2:52

.= (id (rng g)) * g by A8, A23, TOPS_2:def 5

.= g by RELAT_1:54 ;

then A33: f . (((f ") * g) . t) = g . t by A32, FUNCT_1:13;

A34: s1 in dom f by A6, A21, BORSUK_1:43;

s2 in dom g by A12, A13, A28, BORSUK_1:43;

then ((f ") * g) . s2 = (f ") . q1 by A11, FUNCT_1:13

.= s1 by A2, A14, A34, A24, FUNCT_1:32 ;

then ((f ") * g) . s29 = s1 ;

then s1 < Ft by A16, A20, A29, A30, JORDAN5A:15, TOPMETR:20;

hence not g . t in Q by A7, A31, A33; :: thesis: verum

for f being Function of I[01],((TOP-REAL 2) | P)

for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 1 >= t & t > s1 holds

not f . t in Q ) holds

for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q

let p1, p2, q1 be Point of (TOP-REAL 2); :: thesis: for f being Function of I[01],((TOP-REAL 2) | P)

for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 1 >= t & t > s1 holds

not f . t in Q ) holds

for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q

let f be Function of I[01],((TOP-REAL 2) | P); :: thesis: for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 1 >= t & t > s1 holds

not f . t in Q ) holds

for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q

let s1 be Real; :: thesis: ( q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 1 >= t & t > s1 holds

not f . t in Q ) implies for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q )

assume that

A1: q1 in P and

A2: f . s1 = q1 and

A3: f is being_homeomorphism and

A4: f . 0 = p1 and

A5: f . 1 = p2 and

A6: ( 0 <= s1 & s1 <= 1 ) and

A7: for t being Real st 1 >= t & t > s1 holds

not f . t in Q ; :: thesis: for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q

reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1;

let g be Function of I[01],((TOP-REAL 2) | P); :: thesis: for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q

let s2 be Real; :: thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 implies for t being Real st 1 >= t & t > s2 holds

not g . t in Q )

assume that

A8: g is being_homeomorphism and

A9: g . 0 = p1 and

A10: g . 1 = p2 and

A11: g . s2 = q1 and

A12: 0 <= s2 and

A13: s2 <= 1 ; :: thesis: for t being Real st 1 >= t & t > s2 holds

not g . t in Q

reconsider f = f, g = g as Function of I[01],((TOP-REAL 2) | P9) ;

A14: f is one-to-one by A3, TOPS_2:def 5;

set fg = (f ") * g;

let t be Real; :: thesis: ( 1 >= t & t > s2 implies not g . t in Q )

assume that

A15: 1 >= t and

A16: t > s2 ; :: thesis: not g . t in Q

reconsider t1 = t, s29 = s2 as Point of I[01] by A12, A13, A15, A16, BORSUK_1:43;

A17: t in the carrier of I[01] by A12, A15, A16, BORSUK_1:43;

reconsider Ft = ((f ") * g) . t1 as Real by BORSUK_1:40;

A18: rng g = [#] ((TOP-REAL 2) | P) by A8, TOPS_2:def 5;

A19: f " is being_homeomorphism by A3, TOPS_2:56;

then (f ") * g is being_homeomorphism by A8, TOPS_2:57;

then A20: ( (f ") * g is continuous & (f ") * g is one-to-one ) by TOPS_2:def 5;

A21: dom f = [#] I[01] by A3, TOPS_2:def 5;

then A22: 0 in dom f by BORSUK_1:43;

A23: rng f = [#] ((TOP-REAL 2) | P) by A3, TOPS_2:def 5;

then f is onto by FUNCT_2:def 3;

then A24: f " = f " by A14, TOPS_2:def 4;

then A25: (f ") . p1 = 0 by A4, A22, A14, FUNCT_1:32;

A26: 1 in dom f by A21, BORSUK_1:43;

A27: (f ") . p2 = 1 by A24, A5, A26, A14, FUNCT_1:32;

A28: dom g = [#] I[01] by A8, TOPS_2:def 5;

then 0 in dom g by BORSUK_1:43;

then A29: ((f ") * g) . 0 = 0 by A9, A25, FUNCT_1:13;

1 in dom g by A28, BORSUK_1:43;

then A30: ((f ") * g) . 1 = 1 by A10, A27, FUNCT_1:13;

A31: Ft <= 1

proof end;

dom (f ") = [#] ((TOP-REAL 2) | P)
by A19, TOPS_2:def 5;then A32: t in dom ((f ") * g) by A28, A18, A17, RELAT_1:27;

f * ((f ") * g) = g * (f * (f ")) by RELAT_1:36

.= g * (id (rng f)) by A23, A14, TOPS_2:52

.= (id (rng g)) * g by A8, A23, TOPS_2:def 5

.= g by RELAT_1:54 ;

then A33: f . (((f ") * g) . t) = g . t by A32, FUNCT_1:13;

A34: s1 in dom f by A6, A21, BORSUK_1:43;

s2 in dom g by A12, A13, A28, BORSUK_1:43;

then ((f ") * g) . s2 = (f ") . q1 by A11, FUNCT_1:13

.= s1 by A2, A14, A34, A24, FUNCT_1:32 ;

then ((f ") * g) . s29 = s1 ;

then s1 < Ft by A16, A20, A29, A30, JORDAN5A:15, TOPMETR:20;

hence not g . t in Q by A7, A31, A33; :: thesis: verum