let P, Q be Subset of (TOP-REAL 2); :: thesis:
let p1, p2, q1 be Point of (TOP-REAL 2); :: thesis:
let f be Function of I[01] ,((TOP-REAL 2) | P); :: thesis:
let s1 be Real; :: thesis:
assume A1: ( q1 in P & q1 in Q & 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 ) ) ; :: thesis:
let g be Function of I[01] ,((TOP-REAL 2) | P); :: thesis:
let s2 be Real; :: thesis:
reconsider P' = P as non empty Subset of (TOP-REAL 2) by A1;
assume A2: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 ) ; :: thesis:
reconsider f = f, g = g as Function of I[01] ,((TOP-REAL 2) | P') ;
let t be Real; :: thesis:
assume A3: ( 1 >= t & t > s2 ) ; :: thesis:
set fg = (f " ) * g;
A4: f " is being_homeomorphism by A1, TOPS_2:70;
then A5: (f " ) * g is being_homeomorphism by A2, TOPS_2:71;
A6: ( dom f = [#] I[01] & rng f = [#] ((TOP-REAL 2) | P) ) by A1, TOPS_2:def 5;
then A7: ( 0 in dom f & 1 in dom f ) by BORSUK_1:86;
A8: f is one-to-one by A1, TOPS_2:def 5;
A9: ( (f " ) * g is continuous & (f " ) * g is one-to-one ) by A5, TOPS_2:def 5;
A10: (f " ) . p1 = (f " ) . p1 by A6, A8, TOPS_2:def 4
.= 0 by A1, A7, A8, FUNCT_1:54 ;
A11: dom (f " ) = [#] ((TOP-REAL 2) | P) by A4, TOPS_2:def 5;
A12: (f " ) . p2 = (f " ) . p2 by A6, A8, TOPS_2:def 4
.= 1 by A1, A7, A8, FUNCT_1:54 ;
A13: ( dom g = [#] I[01] & rng g = [#] ((TOP-REAL 2) | P) ) by A2, TOPS_2:def 5;
then 0 in dom g by BORSUK_1:86;
then A14: ((f " ) * g) . 0 = 0 by A2, A10, FUNCT_1:23;
1 in dom g by A13, BORSUK_1:86;
then A15: ((f " ) * g) . 1 = 1 by A2, A12, FUNCT_1:23;
A16: s1 in dom f by A1, A6, BORSUK_1:86;
s2 in dom g by A2, A13, BORSUK_1:86;
then A17: ((f " ) * g) . s2 = (f " ) . q1 by A2, FUNCT_1:23
.= (f " ) . q1 by A6, A8, TOPS_2:def 4
.= s1 by A1, A8, A16, FUNCT_1:54 ;
reconsider t1 = t, s2' = s2 as Point of I[01] by A2, A3, BORSUK_1:86;
A18: t in the carrier of I[01] by A2, A3, BORSUK_1:86;
then ((f " ) * g) . t in the carrier of I[01] by FUNCT_2:7;
then reconsider Ft = ((f " ) * g) . t1 as Real by BORSUK_1:83;
A19: Ft <= 1

proof

per cases by A3, XXREAL_0:1;

suppose t < 1 ; :: thesis:

hence Ft <= 1 by A9, A14, A15, BORSUK_1:def 18, JORDAN5A:16, TOPMETR:27; :: thesis:

end;

suppose t = 1 ; :: thesis:

hence Ft <= 1 by A2, A12, A13, FUNCT_1:23; :: thesis:

end;

((f " ) * g) . s2' = s1 by A17;
then A20: s1 < Ft by A3, A9, A14, A15, JORDAN5A:16, TOPMETR:27;
A21: f * ((f " ) * g) = g * (f * (f " )) by RELAT_1:55
.= g * (id (rng f)) by A6, A8, TOPS_2:65
.= (id (rng g)) * g by A2, A6, TOPS_2:def 5
.= g by RELAT_1:80 ;
t in dom ((f " ) * g) by A11, A13, A18, RELAT_1:46;
then f . (((f " ) * g) . t) = g . t by A21, FUNCT_1:23;
hence not g . t in Q by A1, A19, A20; :: thesis: