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 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); :: 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 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); :: 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 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; :: 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 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 ; :: 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 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); :: 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 0 <= 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 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 ; :: thesis: 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:86;
A17: rng f = [#] ((TOP-REAL 2) | P) by A3, TOPS_2:def 5;
then A18: (f ") . p2 = (f ") . p2 by A14, TOPS_2:def 4
.= 1 by A5, A16, A14, FUNCT_1:54 ;
A19: 0 in dom f by A15, BORSUK_1:86;
A20: (f ") . p1 = (f ") . p1 by A17, A14, TOPS_2:def 4
.= 0 by A4, A19, A14, FUNCT_1:54 ;
set fg = (f ") * g;
A21: f " is being_homeomorphism by A3, TOPS_2:70;
then (f ") * g is being_homeomorphism by A8, TOPS_2:71;
then A22: ( (f ") * g is continuous & (f ") * g is one-to-one ) by TOPS_2:def 5;
let t be Real; :: thesis: ( 0 <= t & t < s2 implies not g . t in Q )
assume that
A23: 0 <= t and
A24: t < s2 ; :: thesis: not g . t in Q
A25: t <= 1 by A13, A24, XXREAL_0:2;
then reconsider t1 = t, s29 = s2 as Point of I[01] by A12, A13, A23, BORSUK_1:86;
A26: t in the carrier of I[01] by A23, A25, 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;
A27: rng g = [#] ((TOP-REAL 2) | P) by A8, TOPS_2:def 5;
A28: dom g = [#] I[01] by A8, TOPS_2:def 5;
then 1 in dom g by BORSUK_1:86;
then A29: ((f ") * g) . 1 = 1 by A10, A18, FUNCT_1:23;
A30: s1 in dom f by A6, A15, BORSUK_1:86;
dom (f ") = [#] ((TOP-REAL 2) | P) by A21, TOPS_2:def 5;
then A31: dom ((f ") * g) = dom g by A27, RELAT_1:46;
0 in dom g by A28, BORSUK_1:86;
then A32: ((f ") * g) . 0 = 0 by A9, A20, FUNCT_1:23;
A33: 0 <= Ft

proof

per cases ( 0 < t or 0 = t ) by A23;

suppose 0 < t ; :: thesis: 0 <= Ft

hence 0 <= Ft by A22, A32, A29, BORSUK_1:def 17, JORDAN5A:16, TOPMETR:27; :: thesis: verum

end;

suppose 0 = t ; :: thesis: 0 <= Ft

hence 0 <= Ft by A9, A20, A28, FUNCT_1:23; :: thesis: verum

end;

end;

end;

f * ((f ") * g) = g * (f * (f ")) by RELAT_1:55
.= g * (id (rng f)) by A17, A14, TOPS_2:65
.= (id (rng g)) * g by A8, A17, TOPS_2:def 5
.= g by RELAT_1:80 ;
then A34: f . (((f ") * g) . t) = g . t by A28, A26, A31, FUNCT_1:23;
s2 in dom g by A12, A13, A28, BORSUK_1:86;
then ((f ") * g) . s2 = (f ") . q1 by A11, FUNCT_1:23
.= (f ") . q1 by A17, A14, TOPS_2:def 4
.= s1 by A2, A14, A30, FUNCT_1:54 ;
then ((f ") * g) . s29 = s1 ;
then Ft < s1 by A24, A22, A32, A29, JORDAN5A:16, TOPMETR:27;
hence not g . t in Q by A7, A33, A34; :: thesis: verum