let P, Q be Subset of (TOP-REAL 2); 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 0 <= 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 0 <= t & t < s2 holds
not g . t in Q
let p1, p2, q1 be 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 0 <= 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 0 <= t & t < s2 holds
not g . t in Q
let f be 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 0 <= 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 0 <= t & t < s2 holds
not g . t in Q
let s1 be Real; ( 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 0 <= 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 0 <= 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 0 <= t & t < s1 holds
not f . t in Q
; 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 0 <= 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); 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 0 <= t & t < s2 holds
not g . t in Q
let s2 be Real; ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 implies for t being Real st 0 <= 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
; for t being Real st 0 <= 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;
A15:
dom f = [#] I[01]
by A3, TOPS_2:def 5;
then A16:
1 in dom f
by BORSUK_1:43;
A17:
rng f = [#] ((TOP-REAL 2) | P)
by A3, TOPS_2:def 5;
then
f is onto
by FUNCT_2:def 3;
then A18:
f " = f "
by A14, TOPS_2:def 4;
A19:
(f ") . p2 = 1
by A5, A16, A14, A18, FUNCT_1:32;
A20:
0 in dom f
by A15, BORSUK_1:43;
A21:
(f ") . p1 = 0
by A4, A20, A14, A18, FUNCT_1:32;
set fg = (f ") * g;
A22:
f " is being_homeomorphism
by A3, TOPS_2:56;
then
(f ") * g is being_homeomorphism
by A8, TOPS_2:57;
then A23:
( (f ") * g is continuous & (f ") * g is one-to-one )
by TOPS_2:def 5;
let t be Real; ( 0 <= t & t < s2 implies not g . t in Q )
assume that
A24:
0 <= t
and
A25:
t < s2
; not g . t in Q
A26:
t <= 1
by A13, A25, XXREAL_0:2;
then reconsider t1 = t, s29 = s2 as Point of I[01] by A12, A13, A24, BORSUK_1:43;
A27:
t in the carrier of I[01]
by A24, A26, BORSUK_1:43;
reconsider Ft = ((f ") * g) . t1 as Real by BORSUK_1:40;
A28:
rng g = [#] ((TOP-REAL 2) | P)
by A8, TOPS_2:def 5;
A29:
dom g = [#] I[01]
by A8, TOPS_2:def 5;
then
1 in dom g
by BORSUK_1:43;
then A30:
((f ") * g) . 1 = 1
by A10, A19, FUNCT_1:13;
A31:
s1 in dom f
by A6, A15, BORSUK_1:43;
dom (f ") = [#] ((TOP-REAL 2) | P)
by A22, TOPS_2:def 5;
then A32:
dom ((f ") * g) = dom g
by A28, RELAT_1:27;
0 in dom g
by A29, BORSUK_1:43;
then A33:
((f ") * g) . 0 = 0
by A9, A21, FUNCT_1:13;
A34:
0 <= Ft
f * ((f ") * g) =
g * (f * (f "))
by RELAT_1:36
.=
g * (id (rng f))
by A17, A14, TOPS_2:52
.=
(id (rng g)) * g
by A8, A17, TOPS_2:def 5
.=
g
by RELAT_1:54
;
then A35:
f . (((f ") * g) . t) = g . t
by A29, A27, A32, FUNCT_1:13;
s2 in dom g
by A12, A13, A29, BORSUK_1:43;
then ((f ") * g) . s2 =
(f ") . q1
by A11, FUNCT_1:13
.=
s1
by A2, A14, A31, A18, FUNCT_1:32
;
then
((f ") * g) . s29 = s1
;
then
Ft < s1
by A25, A23, A33, A30, JORDAN5A:15, TOPMETR:20;
hence
not g . t in Q
by A7, A34, A35; verum