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

proof

per cases by A3;

suppose 0 < t ; :: thesis:

hence 0 <= Ft by A10, A15, A16, BORSUK_1:def 17, JORDAN5A:16, TOPMETR:27; :: thesis:

end;

suppose 0 = t ; :: thesis:

hence 0 <= Ft by A2, A11, A14, FUNCT_1:23; :: thesis:

end;

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