let P, Q be Subset of (); :: thesis: for p1, p2, q1 being Point of ()
for f being Function of I,(() | 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,(() | 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 (); :: thesis: for f being Function of I,(() | 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,(() | 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,(() | 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,(() | 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,(() | 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,(() | 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 () by A1;
let g be Function of I,(() | 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,(() | P9) ;
A14: f is one-to-one by ;
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 by ;
A17: t in the carrier of I by ;
reconsider Ft = ((f ") * g) . t1 as Real by BORSUK_1:40;
A18: rng g = [#] (() | P) by ;
A19: f " is being_homeomorphism by ;
then (f ") * g is being_homeomorphism by ;
then A20: ( (f ") * g is continuous & (f ") * g is one-to-one ) by TOPS_2:def 5;
A21: dom f = [#] I by ;
then A22: 0 in dom f by BORSUK_1:43;
A23: rng f = [#] (() | P) by ;
then f is onto by FUNCT_2:def 3;
then A24: f " = f " by ;
then A25: (f ") . p1 = 0 by ;
A26: 1 in dom f by ;
A27: (f ") . p2 = 1 by ;
A28: dom g = [#] I by ;
then 0 in dom g by BORSUK_1:43;
then A29: ((f ") * g) . 0 = 0 by ;
1 in dom g by ;
then A30: ((f ") * g) . 1 = 1 by ;
A31: Ft <= 1
proof
per cases ( t < 1 or t = 1 ) by ;
suppose t < 1 ; :: thesis: Ft <= 1
hence Ft <= 1 by ; :: thesis: verum
end;
suppose t = 1 ; :: thesis: Ft <= 1
hence Ft <= 1 by ; :: thesis: verum
end;
end;
end;
dom (f ") = [#] (() | P) by ;
then A32: t in dom ((f ") * g) by ;
f * ((f ") * g) = g * (f * (f ")) by RELAT_1:36
.= g * (id (rng f)) by
.= (id (rng g)) * g by
.= g by RELAT_1:54 ;
then A33: f . (((f ") * g) . t) = g . t by ;
A34: s1 in dom f by ;
s2 in dom g by ;
then ((f ") * g) . s2 = (f ") . q1 by
.= s1 by ;
then ((f ") * g) . s29 = s1 ;
then s1 < Ft by ;
hence not g . t in Q by A7, A31, A33; :: thesis: verum