let a, b, c, d be real number ; :: thesis:
set K = rectangle a,b,c,d;
assume A1: ( a < b & c < d ) ; :: thesis:
defpred S₁[ set , set ] means for r being Real st $1 = r holds
( ( r in [.0 ,(1 / 2).] implies $2 = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) ) & ( r in [.(1 / 2),1.] implies $2 = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) ) );
A2: [.0 ,1.] = [.0 ,(1 / 2).] \/ [.(1 / 2),1.] by XXREAL_1:165;
A7: for x being set st x in [.0 ,1.] holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis:
assume A8: x in [.0 ,1.] ; :: thesis:

now

per cases by A2, A8, XBOOLE_0:def 3;

case A9: x in [.0 ,(1 / 2).] ; :: thesis:

then reconsider r = x as Real ;
A10: ( 0 <= r & r <= 1 / 2 ) by A9, XXREAL_1:1;
set y0 = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|);
( r in [.(1 / 2),1.] implies ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) )

proof

assume r in [.(1 / 2),1.] ; :: thesis:
then ( 1 / 2 <= r & r <= 1 ) by XXREAL_1:1;
then A11: r = 1 / 2 by A10, XXREAL_0:1;
then A12: ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) = (0 * |[a,c]|) + |[a,d]| by EUCLID:33
.= (0. (TOP-REAL 2)) + |[a,d]| by EUCLID:33
.= |[a,d]| by EUCLID:31 ;
((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) = (1 * |[a,d]|) + (0. (TOP-REAL 2)) by A11, EUCLID:33
.= |[a,d]| + (0. (TOP-REAL 2)) by EUCLID:33
.= |[a,d]| by EUCLID:31 ;
hence ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) by A12; :: thesis:

end;

then for r2 being Real st x = r2 holds
( ( r2 in [.0 ,(1 / 2).] implies ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) = ((1 - (2 * r2)) * |[a,c]|) + ((2 * r2) * |[a,d]|) ) & ( r2 in [.(1 / 2),1.] implies ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) = ((1 - ((2 * r2) - 1)) * |[a,d]|) + (((2 * r2) - 1) * |[b,d]|) ) ) ;
hence ex y being set st S₁[x,y] ; :: thesis:

end;

case A13: x in [.(1 / 2),1.] ; :: thesis:

then reconsider r = x as Real ;
A14: ( 1 / 2 <= r & r <= 1 ) by A13, XXREAL_1:1;
set y0 = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|);
( r in [.0 ,(1 / 2).] implies ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) )

proof

assume r in [.0 ,(1 / 2).] ; :: thesis:
then ( 0 <= r & r <= 1 / 2 ) by XXREAL_1:1;
then A15: r = 1 / 2 by A14, XXREAL_0:1;
then A16: ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) = |[a,d]| + (0 * |[b,d]|) by EUCLID:33
.= |[a,d]| + (0. (TOP-REAL 2)) by EUCLID:33
.= |[a,d]| by EUCLID:31 ;
((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) = (0. (TOP-REAL 2)) + (1 * |[a,d]|) by A15, EUCLID:33
.= (0. (TOP-REAL 2)) + |[a,d]| by EUCLID:33
.= |[a,d]| by EUCLID:31 ;
hence ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) by A16; :: thesis:

end;

then for r2 being Real st x = r2 holds
( ( r2 in [.0 ,(1 / 2).] implies ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) = ((1 - (2 * r2)) * |[a,c]|) + ((2 * r2) * |[a,d]|) ) & ( r2 in [.(1 / 2),1.] implies ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) = ((1 - ((2 * r2) - 1)) * |[a,d]|) + (((2 * r2) - 1) * |[b,d]|) ) ) ;
hence ex y being set st S₁[x,y] ; :: thesis:

end;

hence ex y being set st S₁[x,y] ; :: thesis:

end;

ex f2 being Function st
( dom f2 = [.0 ,1.] & ( for x being set st x in [.0 ,1.] holds
S₁[x,f2 . x] ) ) from CLASSES1:sch 1(A7);
then consider f2 being Function such that
A17: ( dom f2 = [.0 ,1.] & ( for x being set st x in [.0 ,1.] holds
S₁[x,f2 . x] ) ) ;
rng f2 c= the carrier of ((TOP-REAL 2) | (Upper_Arc (rectangle a,b,c,d)))

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f2 ; :: thesis:
then consider x being set such that
A18: ( x in dom f2 & y = f2 . x ) by FUNCT_1:def 5;

now

per cases by A2, A17, A18, XBOOLE_0:def 3;

case A19: x in [.0 ,(1 / 2).] ; :: thesis:

then reconsider r = x as Real ;
A20: ( 0 <= r & r <= 1 / 2 ) by A19, XXREAL_1:1;
then A21: r * 2 <= (1 / 2) * 2 by XREAL_1:66;
A22: 2 * 0 <= 2 * r by A20;
f2 . x = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) by A17, A18, A19;
then A23: y in { (((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A18, A21, A22;
Upper_Arc (rectangle a,b,c,d) = (LSeg |[a,c]|,|[a,d]|) \/ (LSeg |[a,d]|,|[b,d]|) by A1, Th61;
then y in Upper_Arc (rectangle a,b,c,d) by A23, XBOOLE_0:def 3;
hence y in the carrier of ((TOP-REAL 2) | (Upper_Arc (rectangle a,b,c,d))) by PRE_TOPC:29; :: thesis:

end;

case A24: x in [.(1 / 2),1.] ; :: thesis:

then reconsider r = x as Real ;
A25: ( 1 / 2 <= r & r <= 1 ) by A24, XXREAL_1:1;
then r * 2 >= (1 / 2) * 2 by XREAL_1:66;
then A26: (2 * r) - 1 >= 0 by XREAL_1:50;
2 * 1 >= 2 * r by A25, XREAL_1:66;
then A27: (1 + 1) - 1 >= (2 * r) - 1 by XREAL_1:11;
f2 . x = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) by A17, A18, A24;
then A28: y in { (((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A18, A26, A27;
Upper_Arc (rectangle a,b,c,d) = (LSeg |[a,c]|,|[a,d]|) \/ (LSeg |[a,d]|,|[b,d]|) by A1, Th61;
then y in Upper_Arc (rectangle a,b,c,d) by A28, XBOOLE_0:def 3;
hence y in the carrier of ((TOP-REAL 2) | (Upper_Arc (rectangle a,b,c,d))) by PRE_TOPC:29; :: thesis:

end;

hence y in the carrier of ((TOP-REAL 2) | (Upper_Arc (rectangle a,b,c,d))) ; :: thesis:

end;

then reconsider f3 = f2 as Function of I[01] ,((TOP-REAL 2) | (Upper_Arc (rectangle a,b,c,d))) by A17, BORSUK_1:83, FUNCT_2:4;
A29: 0 in [.0 ,1.] by XXREAL_1:1;
0 in [.0 ,(1 / 2).] by XXREAL_1:1;
then A30: f3 . 0 = ((1 - (2 * 0 )) * |[a,c]|) + ((2 * 0 ) * |[a,d]|) by A17, A29
.= (1 * |[a,c]|) + (0. (TOP-REAL 2)) by EUCLID:33
.= |[a,c]| + (0. (TOP-REAL 2)) by EUCLID:33
.= |[a,c]| by EUCLID:31
.= W-min (rectangle a,b,c,d) by A1, Th56 ;
A31: 1 in [.0 ,1.] by XXREAL_1:1;
1 in [.(1 / 2),1.] by XXREAL_1:1;
then A32: f3 . 1 = ((1 - ((2 * 1) - 1)) * |[a,d]|) + (((2 * 1) - 1) * |[b,d]|) by A17, A31
.= (0 * |[a,d]|) + |[b,d]| by EUCLID:33
.= (0. (TOP-REAL 2)) + |[b,d]| by EUCLID:33
.= |[b,d]| by EUCLID:31
.= E-max (rectangle a,b,c,d) by A1, Th56 ;
A33: for r being Real st r in [.0 ,(1 / 2).] holds
f3 . r = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|)

proof

let r be Real; :: thesis:
assume A34: r in [.0 ,(1 / 2).] ; :: thesis:
then A35: ( 0 <= r & r <= 1 / 2 ) by XXREAL_1:1;
then r <= 1 by XXREAL_0:2;
then r in [.0 ,1.] by A35, XXREAL_1:1;
hence f3 . r = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) by A17, A34; :: thesis:

end;

A36: for r being Real st r in [.(1 / 2),1.] holds
f3 . r = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|)

proof

let r be Real; :: thesis:
assume A37: r in [.(1 / 2),1.] ; :: thesis:
then ( 1 / 2 <= r & r <= 1 ) by XXREAL_1:1;
then r in [.0 ,1.] by XXREAL_1:1;
hence f3 . r = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) by A17, A37; :: thesis:

end;

A38: for p being Point of (TOP-REAL 2) st p in LSeg |[a,c]|,|[a,d]| holds
( 0 <= (((p `2 ) - c) / (d - c)) / 2 & (((p `2 ) - c) / (d - c)) / 2 <= 1 & f3 . ((((p `2 ) - c) / (d - c)) / 2) = p )

proof

let p be Point of (TOP-REAL 2); :: thesis:
assume A39: p in LSeg |[a,c]|,|[a,d]| ; :: thesis:
A40: |[a,c]| `2 = c by EUCLID:56;
|[a,d]| `2 = d by EUCLID:56;
then A41: ( c <= p `2 & p `2 <= d ) by A1, A39, A40, TOPREAL1:10;
A42: d - c > 0 by A1, XREAL_1:52;
(p `2 ) - c >= 0 by A41, XREAL_1:50;
then ((p `2 ) - c) / (d - c) >= 0 / (d - c) by A42;
then A43: (((p `2 ) - c) / (d - c)) / 2 >= 0 / 2 ;
A44: d - c > 0 by A1, XREAL_1:52;
(p `2 ) - c <= d - c by A41, XREAL_1:11;
then ((p `2 ) - c) / (d - c) <= (d - c) / (d - c) by A44, XREAL_1:74;
then ((p `2 ) - c) / (d - c) <= 1 by A44, XCMPLX_1:60;
then A45: (((p `2 ) - c) / (d - c)) / 2 <= 1 / 2 by XREAL_1:74;
set r = (((p `2 ) - c) / (d - c)) / 2;
(((p `2 ) - c) / (d - c)) / 2 in [.0 ,(1 / 2).] by A43, A45, XXREAL_1:1;
then f3 . ((((p `2 ) - c) / (d - c)) / 2) = ((1 - (2 * ((((p `2 ) - c) / (d - c)) / 2))) * |[a,c]|) + ((2 * ((((p `2 ) - c) / (d - c)) / 2)) * |[a,d]|) by A33
.= |[((1 - (2 * ((((p `2 ) - c) / (d - c)) / 2))) * a),((1 - (2 * ((((p `2 ) - c) / (d - c)) / 2))) * c)]| + ((2 * ((((p `2 ) - c) / (d - c)) / 2)) * |[a,d]|) by EUCLID:62
.= |[((1 - (2 * ((((p `2 ) - c) / (d - c)) / 2))) * a),((1 - (2 * ((((p `2 ) - c) / (d - c)) / 2))) * c)]| + |[((2 * ((((p `2 ) - c) / (d - c)) / 2)) * a),((2 * ((((p `2 ) - c) / (d - c)) / 2)) * d)]| by EUCLID:62
.= |[(((1 * a) - ((2 * ((((p `2 ) - c) / (d - c)) / 2)) * a)) + ((2 * ((((p `2 ) - c) / (d - c)) / 2)) * a)),(((1 - (2 * ((((p `2 ) - c) / (d - c)) / 2))) * c) + ((2 * ((((p `2 ) - c) / (d - c)) / 2)) * d))]| by EUCLID:60
.= |[a,((1 * c) + ((((p `2 ) - c) / (d - c)) * (d - c)))]|
.= |[a,((1 * c) + ((p `2 ) - c))]| by A44, XCMPLX_1:88
.= |[(p `1 ),(p `2 )]| by A39, TOPREAL3:17
.= p by EUCLID:57 ;
hence ( 0 <= (((p `2 ) - c) / (d - c)) / 2 & (((p `2 ) - c) / (d - c)) / 2 <= 1 & f3 . ((((p `2 ) - c) / (d - c)) / 2) = p ) by A43, A45, XXREAL_0:2; :: thesis:

end;

A46: for p being Point of (TOP-REAL 2) st p in LSeg |[a,d]|,|[b,d]| holds
( 0 <= ((((p `1 ) - a) / (b - a)) / 2) + (1 / 2) & ((((p `1 ) - a) / (b - a)) / 2) + (1 / 2) <= 1 & f3 . (((((p `1 ) - a) / (b - a)) / 2) + (1 / 2)) = p )

proof

let p be Point of (TOP-REAL 2); :: thesis:
assume A47: p in LSeg |[a,d]|,|[b,d]| ; :: thesis:
A48: |[a,d]| `1 = a by EUCLID:56;
|[b,d]| `1 = b by EUCLID:56;
then A49: ( a <= p `1 & p `1 <= b ) by A1, A47, A48, TOPREAL1:9;
A50: b - a > 0 by A1, XREAL_1:52;
(p `1 ) - a >= 0 by A49, XREAL_1:50;
then ((p `1 ) - a) / (b - a) >= 0 / (b - a) by A50;
then (((p `1 ) - a) / (b - a)) / 2 >= 0 / 2 ;
then A51: ((((p `1 ) - a) / (b - a)) / 2) + (1 / 2) >= 0 + (1 / 2) by XREAL_1:9;
A52: b - a > 0 by A1, XREAL_1:52;
(p `1 ) - a <= b - a by A49, XREAL_1:11;
then ((p `1 ) - a) / (b - a) <= (b - a) / (b - a) by A52, XREAL_1:74;
then ((p `1 ) - a) / (b - a) <= 1 by A52, XCMPLX_1:60;
then (((p `1 ) - a) / (b - a)) / 2 <= 1 / 2 by XREAL_1:74;
then A53: ((((p `1 ) - a) / (b - a)) / 2) + (1 / 2) <= (1 / 2) + (1 / 2) by XREAL_1:9;
set r = ((((p `1 ) - a) / (b - a)) / 2) + (1 / 2);
((((p `1 ) - a) / (b - a)) / 2) + (1 / 2) in [.(1 / 2),1.] by A51, A53, XXREAL_1:1;
then f3 . (((((p `1 ) - a) / (b - a)) / 2) + (1 / 2)) = ((1 - ((2 * (((((p `1 ) - a) / (b - a)) / 2) + (1 / 2))) - 1)) * |[a,d]|) + (((2 * (((((p `1 ) - a) / (b - a)) / 2) + (1 / 2))) - 1) * |[b,d]|) by A36
.= |[((1 - ((2 * (((((p `1 ) - a) / (b - a)) / 2) + (1 / 2))) - 1)) * a),((1 - ((2 * (((((p `1 ) - a) / (b - a)) / 2) + (1 / 2))) - 1)) * d)]| + (((2 * (((((p `1 ) - a) / (b - a)) / 2) + (1 / 2))) - 1) * |[b,d]|) by EUCLID:62
.= |[((1 - ((2 * (((((p `1 ) - a) / (b - a)) / 2) + (1 / 2))) - 1)) * a),((1 - ((2 * (((((p `1 ) - a) / (b - a)) / 2) + (1 / 2))) - 1)) * d)]| + |[(((2 * (((((p `1 ) - a) / (b - a)) / 2) + (1 / 2))) - 1) * b),(((2 * (((((p `1 ) - a) / (b - a)) / 2) + (1 / 2))) - 1) * d)]| by EUCLID:62
.= |[(((1 - ((2 * (((((p `1 ) - a) / (b - a)) / 2) + (1 / 2))) - 1)) * a) + (((2 * (((((p `1 ) - a) / (b - a)) / 2) + (1 / 2))) - 1) * b)),(((1 * d) - (((2 * (((((p `1 ) - a) / (b - a)) / 2) + (1 / 2))) - 1) * d)) + (((2 * (((((p `1 ) - a) / (b - a)) / 2) + (1 / 2))) - 1) * d))]| by EUCLID:60
.= |[((1 * a) + ((((p `1 ) - a) / (b - a)) * (b - a))),d]|
.= |[((1 * a) + ((p `1 ) - a)),d]| by A52, XCMPLX_1:88
.= |[(p `1 ),(p `2 )]| by A47, TOPREAL3:18
.= p by EUCLID:57 ;
hence ( 0 <= ((((p `1 ) - a) / (b - a)) / 2) + (1 / 2) & ((((p `1 ) - a) / (b - a)) / 2) + (1 / 2) <= 1 & f3 . (((((p `1 ) - a) / (b - a)) / 2) + (1 / 2)) = p ) by A51, A53; :: thesis:

end;

reconsider B00 = [.0 ,1.] as Subset of R^1 by TOPMETR:24;
reconsider B01 = B00 as non empty Subset of R^1 by XXREAL_1:1;
I[01] = R^1 | B01 by TOPMETR:26, TOPMETR:27;
then consider h1 being Function of I[01] ,R^1 such that
A54: ( ( for p being Point of I[01] holds h1 . p = p ) & h1 is continuous ) by Th14;
consider h2 being Function of I[01] ,R^1 such that
A55: ( ( for p being Point of I[01]
for r1 being real number st h1 . p = r1 holds
h2 . p = 2 * r1 ) & h2 is continuous ) by A54, JGRAPH_2:33;
consider h5 being Function of I[01] ,R^1 such that
A56: ( ( for p being Point of I[01]
for r1 being real number st h2 . p = r1 holds
h5 . p = 1 - r1 ) & h5 is continuous ) by A55, Th16;
consider h3 being Function of I[01] ,R^1 such that
A57: ( ( for p being Point of I[01]
for r1 being real number st h2 . p = r1 holds
h3 . p = r1 - 1 ) & h3 is continuous ) by A55, Th15;
consider h4 being Function of I[01] ,R^1 such that
A58: ( ( for p being Point of I[01]
for r1 being real number st h3 . p = r1 holds
h4 . p = 1 - r1 ) & h4 is continuous ) by A57, Th16;
consider g1 being Function of I[01] ,(TOP-REAL 2) such that
A59: ( ( for r being Point of I[01] holds g1 . r = ((h5 . r) * |[a,c]|) + ((h2 . r) * |[a,d]|) ) & g1 is continuous ) by A55, A56, Th21;
A60: for r being Point of I[01]
for s being real number st r = s holds
g1 . r = ((1 - (2 * s)) * |[a,c]|) + ((2 * s) * |[a,d]|)

proof

let r be Point of I[01] ; :: thesis:
let s be real number ; :: thesis:
assume A61: r = s ; :: thesis:
g1 . r = ((h5 . r) * |[a,c]|) + ((h2 . r) * |[a,d]|) by A59
.= ((1 - (2 * (h1 . r))) * |[a,c]|) + ((h2 . r) * |[a,d]|) by A55, A56
.= ((1 - (2 * (h1 . r))) * |[a,c]|) + ((2 * (h1 . r)) * |[a,d]|) by A55
.= ((1 - (2 * s)) * |[a,c]|) + ((2 * (h1 . r)) * |[a,d]|) by A54, A61
.= ((1 - (2 * s)) * |[a,c]|) + ((2 * s) * |[a,d]|) by A54, A61 ;
hence g1 . r = ((1 - (2 * s)) * |[a,c]|) + ((2 * s) * |[a,d]|) ; :: thesis:

end;

consider g2 being Function of I[01] ,(TOP-REAL 2) such that
A62: ( ( for r being Point of I[01] holds g2 . r = ((h4 . r) * |[a,d]|) + ((h3 . r) * |[b,d]|) ) & g2 is continuous ) by A57, A58, Th21;
A63: for r being Point of I[01]
for s being real number st r = s holds
g2 . r = ((1 - ((2 * s) - 1)) * |[a,d]|) + (((2 * s) - 1) * |[b,d]|)

proof

let r be Point of I[01] ; :: thesis:
let s be real number ; :: thesis:
assume A64: r = s ; :: thesis:
g2 . r = ((h4 . r) * |[a,d]|) + ((h3 . r) * |[b,d]|) by A62
.= ((1 - ((h2 . r) - 1)) * |[a,d]|) + ((h3 . r) * |[b,d]|) by A57, A58
.= ((1 - ((h2 . r) - 1)) * |[a,d]|) + (((h2 . r) - 1) * |[b,d]|) by A57
.= ((1 - ((2 * (h1 . r)) - 1)) * |[a,d]|) + (((h2 . r) - 1) * |[b,d]|) by A55
.= ((1 - ((2 * (h1 . r)) - 1)) * |[a,d]|) + (((2 * (h1 . r)) - 1) * |[b,d]|) by A55
.= ((1 - ((2 * s) - 1)) * |[a,d]|) + (((2 * (h1 . r)) - 1) * |[b,d]|) by A54, A64
.= ((1 - ((2 * s) - 1)) * |[a,d]|) + (((2 * s) - 1) * |[b,d]|) by A54, A64 ;
hence g2 . r = ((1 - ((2 * s) - 1)) * |[a,d]|) + (((2 * s) - 1) * |[b,d]|) ; :: thesis:

end;

reconsider B11 = [.0 ,(1 / 2).] as non empty Subset of I[01] by A2, BORSUK_1:83, XBOOLE_1:7, XXREAL_1:1;
A65: dom (g1 | B11) = (dom g1) /\ B11 by RELAT_1:90
.= the carrier of I[01] /\ B11 by FUNCT_2:def 1
.= B11 by XBOOLE_1:28
.= the carrier of (I[01] | B11) by PRE_TOPC:29 ;
rng (g1 | B11) c= the carrier of (TOP-REAL 2) ;
then reconsider g11 = g1 | B11 as Function of (I[01] | B11),(TOP-REAL 2) by A65, FUNCT_2:4;
X: TOP-REAL 2 is SubSpace of TOP-REAL 2 by TSEP_1:2;
then A67: g11 is continuous by A59, BORSUK_4:69;
reconsider B22 = [.(1 / 2),1.] as non empty Subset of I[01] by A2, BORSUK_1:83, XBOOLE_1:7, XXREAL_1:1;
A68: dom (g2 | B22) = (dom g2) /\ B22 by RELAT_1:90
.= the carrier of I[01] /\ B22 by FUNCT_2:def 1
.= B22 by XBOOLE_1:28
.= the carrier of (I[01] | B22) by PRE_TOPC:29 ;
rng (g2 | B22) c= the carrier of (TOP-REAL 2) ;
then reconsider g22 = g2 | B22 as Function of (I[01] | B22),(TOP-REAL 2) by A68, FUNCT_2:4;
A69: g22 is continuous by X, A62, BORSUK_4:69;
A70: B11 = [#] (I[01] | B11) by PRE_TOPC:def 10;
A71: B22 = [#] (I[01] | B22) by PRE_TOPC:def 10;
A72: B11 is closed by Th12;
A73: B22 is closed by Th12;
B11 \/ B22 = [.0 ,1.] by XXREAL_1:165;
then A74: ([#] (I[01] | B11)) \/ ([#] (I[01] | B22)) = [#] I[01] by A70, A71, BORSUK_1:83;
for p being set st p in ([#] (I[01] | B11)) /\ ([#] (I[01] | B22)) holds
g11 . p = g22 . p

proof

let p be set ; :: thesis:
assume p in ([#] (I[01] | B11)) /\ ([#] (I[01] | B22)) ; :: thesis:
then ( p in [#] (I[01] | B11) & p in [#] (I[01] | B22) ) by XBOOLE_0:def 4;
then A75: ( p in B11 & p in B22 ) by PRE_TOPC:def 10;
then reconsider rp = p as Real ;
A76: rp <= 1 / 2 by A75, XXREAL_1:1;
rp >= 1 / 2 by A75, XXREAL_1:1;
then rp = 1 / 2 by A76, XXREAL_0:1;
then A77: 2 * rp = 1 ;
thus g11 . p = g1 . p by A75, FUNCT_1:72
.= ((1 - 1) * |[a,c]|) + (1 * |[a,d]|) by A60, A75, A77
.= (0. (TOP-REAL 2)) + (1 * |[a,d]|) by EUCLID:33
.= ((1 - 0 ) * |[a,d]|) + ((1 - 1) * |[b,d]|) by EUCLID:33
.= g2 . p by A63, A75, A77
.= g22 . p by A75, FUNCT_1:72 ; :: thesis:

end;

then consider h being Function of I[01] ,(TOP-REAL 2) such that
A78: ( h = g11 +* g22 & h is continuous ) by A67, A69, A70, A71, A72, A73, A74, JGRAPH_2:9;
A79: ( dom f3 = dom h & dom f3 = the carrier of I[01] ) by Th13;
for x being set st x in dom f2 holds
f3 . x = h . x

proof

let x be set ; :: thesis:
assume A80: x in dom f2 ; :: thesis:
then reconsider rx = x as Real by A79, BORSUK_1:83;
A81: ( 0 <= rx & rx <= 1 ) by A79, A80, BORSUK_1:83, XXREAL_1:1;

now

per cases ;

case A82: rx < 1 / 2 ; :: thesis:

then A83: rx in [.0 ,(1 / 2).] by A81, XXREAL_1:1;
not rx in dom g22 by A71, A82, XXREAL_1:1;
then h . rx = g11 . rx by A78, FUNCT_4:12
.= g1 . rx by A83, FUNCT_1:72
.= ((1 - (2 * rx)) * |[a,c]|) + ((2 * rx) * |[a,d]|) by A60, A79, A80
.= f3 . rx by A33, A83 ;
hence f3 . x = h . x ; :: thesis:

end;

case rx >= 1 / 2 ; :: thesis:

then A84: rx in [.(1 / 2),1.] by A81, XXREAL_1:1;
then rx in [#] (I[01] | B22) by PRE_TOPC:def 10;
then h . rx = g22 . rx by A68, A78, FUNCT_4:14
.= g2 . rx by A84, FUNCT_1:72
.= ((1 - ((2 * rx) - 1)) * |[a,d]|) + (((2 * rx) - 1) * |[b,d]|) by A63, A79, A80
.= f3 . rx by A36, A84 ;
hence f3 . x = h . x ; :: thesis:

end;

hence f3 . x = h . x ; :: thesis:

end;

then A85: f2 = h by A79, FUNCT_1:9;
A86: dom f3 = [#] I[01] by A17, BORSUK_1:83;
for x1, x2 being set st x1 in dom f3 & x2 in dom f3 & f3 . x1 = f3 . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis:
assume A87: ( x1 in dom f3 & x2 in dom f3 & f3 . x1 = f3 . x2 ) ; :: thesis:
then reconsider r1 = x1 as Real by A17;
reconsider r2 = x2 as Real by A17, A87;
A88: (LSeg |[a,c]|,|[a,d]|) /\ (LSeg |[a,d]|,|[b,d]|) = {|[a,d]|} by A1, Th44;

now

per cases by A2, A17, A87, XBOOLE_0:def 3;

case A89: ( x1 in [.0 ,(1 / 2).] & x2 in [.0 ,(1 / 2).] ) ; :: thesis:

then f3 . r1 = ((1 - (2 * r1)) * |[a,c]|) + ((2 * r1) * |[a,d]|) by A33;
then ((1 - (2 * r2)) * |[a,c]|) + ((2 * r2) * |[a,d]|) = ((1 - (2 * r1)) * |[a,c]|) + ((2 * r1) * |[a,d]|) by A33, A87, A89;
then (((1 - (2 * r2)) * |[a,c]|) + ((2 * r2) * |[a,d]|)) - ((2 * r1) * |[a,d]|) = (1 - (2 * r1)) * |[a,c]| by EUCLID:52;
then ((1 - (2 * r2)) * |[a,c]|) + (((2 * r2) * |[a,d]|) - ((2 * r1) * |[a,d]|)) = (1 - (2 * r1)) * |[a,c]| by EUCLID:49;
then ((1 - (2 * r2)) * |[a,c]|) + (((2 * r2) - (2 * r1)) * |[a,d]|) = (1 - (2 * r1)) * |[a,c]| by EUCLID:54;
then (((2 * r2) - (2 * r1)) * |[a,d]|) + (((1 - (2 * r2)) * |[a,c]|) - ((1 - (2 * r1)) * |[a,c]|)) = ((1 - (2 * r1)) * |[a,c]|) - ((1 - (2 * r1)) * |[a,c]|) by EUCLID:49;
then (((2 * r2) - (2 * r1)) * |[a,d]|) + (((1 - (2 * r2)) * |[a,c]|) - ((1 - (2 * r1)) * |[a,c]|)) = 0. (TOP-REAL 2) by EUCLID:46;
then (((2 * r2) - (2 * r1)) * |[a,d]|) + (((1 - (2 * r2)) - (1 - (2 * r1))) * |[a,c]|) = 0. (TOP-REAL 2) by EUCLID:54;
then (((2 * r2) - (2 * r1)) * |[a,d]|) + ((- ((2 * r2) - (2 * r1))) * |[a,c]|) = 0. (TOP-REAL 2) ;
then (((2 * r2) - (2 * r1)) * |[a,d]|) + (- (((2 * r2) - (2 * r1)) * |[a,c]|)) = 0. (TOP-REAL 2) by EUCLID:44;
then (((2 * r2) - (2 * r1)) * |[a,d]|) - (((2 * r2) - (2 * r1)) * |[a,c]|) = 0. (TOP-REAL 2) by EUCLID:45;
then ((2 * r2) - (2 * r1)) * (|[a,d]| - |[a,c]|) = 0. (TOP-REAL 2) by EUCLID:53;
then ( (2 * r2) - (2 * r1) = 0 or |[a,d]| - |[a,c]| = 0. (TOP-REAL 2) ) by EUCLID:35;
then ( (2 * r2) - (2 * r1) = 0 or |[a,d]| = |[a,c]| ) by EUCLID:47;
then ( (2 * r2) - (2 * r1) = 0 or d = |[a,c]| `2 ) by EUCLID:56;
hence x1 = x2 by A1, EUCLID:56; :: thesis:

end;

case A90: ( x1 in [.0 ,(1 / 2).] & x2 in [.(1 / 2),1.] ) ; :: thesis:

then A91: f3 . r1 = ((1 - (2 * r1)) * |[a,c]|) + ((2 * r1) * |[a,d]|) by A33;
A92: ( 0 <= r1 & r1 <= 1 / 2 ) by A90, XXREAL_1:1;
then A93: r1 * 2 <= (1 / 2) * 2 by XREAL_1:66;
2 * 0 <= 2 * r1 by A92;
then A94: f3 . r1 in LSeg |[a,c]|,|[a,d]| by A91, A93;
A95: f3 . r2 = ((1 - ((2 * r2) - 1)) * |[a,d]|) + (((2 * r2) - 1) * |[b,d]|) by A36, A90;
A96: ( 1 / 2 <= r2 & r2 <= 1 ) by A90, XXREAL_1:1;
then r2 * 2 >= (1 / 2) * 2 by XREAL_1:66;
then A97: (2 * r2) - 1 >= 0 by XREAL_1:50;
2 * 1 >= 2 * r2 by A96, XREAL_1:66;
then (1 + 1) - 1 >= (2 * r2) - 1 by XREAL_1:11;
then f3 . r2 in { (((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A95, A97;
then f3 . r1 in (LSeg |[a,c]|,|[a,d]|) /\ (LSeg |[a,d]|,|[b,d]|) by A87, A94, XBOOLE_0:def 4;
then A98: f3 . r1 = |[a,d]| by A88, TARSKI:def 1;
then (((1 - (2 * r1)) * |[a,c]|) + ((2 * r1) * |[a,d]|)) + (- |[a,d]|) = 0. (TOP-REAL 2) by A91, EUCLID:40;
then (((1 - (2 * r1)) * |[a,c]|) + ((2 * r1) * |[a,d]|)) + ((- 1) * |[a,d]|) = 0. (TOP-REAL 2) by EUCLID:43;
then ((1 - (2 * r1)) * |[a,c]|) + (((2 * r1) * |[a,d]|) + ((- 1) * |[a,d]|)) = 0. (TOP-REAL 2) by EUCLID:30;
then ((1 - (2 * r1)) * |[a,c]|) + (((2 * r1) + (- 1)) * |[a,d]|) = 0. (TOP-REAL 2) by EUCLID:37;
then ((1 - (2 * r1)) * |[a,c]|) + ((- (1 - (2 * r1))) * |[a,d]|) = 0. (TOP-REAL 2) ;
then ((1 - (2 * r1)) * |[a,c]|) + (- ((1 - (2 * r1)) * |[a,d]|)) = 0. (TOP-REAL 2) by EUCLID:44;
then ((1 - (2 * r1)) * |[a,c]|) - ((1 - (2 * r1)) * |[a,d]|) = 0. (TOP-REAL 2) by EUCLID:45;
then (1 - (2 * r1)) * (|[a,c]| - |[a,d]|) = 0. (TOP-REAL 2) by EUCLID:53;
then ( 1 - (2 * r1) = 0 or |[a,c]| - |[a,d]| = 0. (TOP-REAL 2) ) by EUCLID:35;
then ( 1 - (2 * r1) = 0 or |[a,c]| = |[a,d]| ) by EUCLID:47;
then A99: ( 1 - (2 * r1) = 0 or c = |[a,d]| `2 ) by EUCLID:56;
(((1 - ((2 * r2) - 1)) * |[a,d]|) + (((2 * r2) - 1) * |[b,d]|)) + (- |[a,d]|) = 0. (TOP-REAL 2) by A87, A95, A98, EUCLID:40;
then (((1 - ((2 * r2) - 1)) * |[a,d]|) + (((2 * r2) - 1) * |[b,d]|)) + ((- 1) * |[a,d]|) = 0. (TOP-REAL 2) by EUCLID:43;
then (((2 * r2) - 1) * |[b,d]|) + (((1 - ((2 * r2) - 1)) * |[a,d]|) + ((- 1) * |[a,d]|)) = 0. (TOP-REAL 2) by EUCLID:30;
then (((2 * r2) - 1) * |[b,d]|) + (((1 - ((2 * r2) - 1)) + (- 1)) * |[a,d]|) = 0. (TOP-REAL 2) by EUCLID:37;
then (((2 * r2) - 1) * |[b,d]|) + ((- ((2 * r2) - 1)) * |[a,d]|) = 0. (TOP-REAL 2) ;
then (((2 * r2) - 1) * |[b,d]|) + (- (((2 * r2) - 1) * |[a,d]|)) = 0. (TOP-REAL 2) by EUCLID:44;
then (((2 * r2) - 1) * |[b,d]|) - (((2 * r2) - 1) * |[a,d]|) = 0. (TOP-REAL 2) by EUCLID:45;
then ((2 * r2) - 1) * (|[b,d]| - |[a,d]|) = 0. (TOP-REAL 2) by EUCLID:53;
then ( (2 * r2) - 1 = 0 or |[b,d]| - |[a,d]| = 0. (TOP-REAL 2) ) by EUCLID:35;
then ( (2 * r2) - 1 = 0 or |[b,d]| = |[a,d]| ) by EUCLID:47;
then ( (2 * r2) - 1 = 0 or b = |[a,d]| `1 ) by EUCLID:56;
hence x1 = x2 by A1, A99, EUCLID:56; :: thesis:

end;

case A100: ( x1 in [.(1 / 2),1.] & x2 in [.0 ,(1 / 2).] ) ; :: thesis:

then A101: f3 . r2 = ((1 - (2 * r2)) * |[a,c]|) + ((2 * r2) * |[a,d]|) by A33;
A102: ( 0 <= r2 & r2 <= 1 / 2 ) by A100, XXREAL_1:1;
then A103: r2 * 2 <= (1 / 2) * 2 by XREAL_1:66;
2 * 0 <= 2 * r2 by A102;
then A104: f3 . r2 in LSeg |[a,c]|,|[a,d]| by A101, A103;
A105: f3 . r1 = ((1 - ((2 * r1) - 1)) * |[a,d]|) + (((2 * r1) - 1) * |[b,d]|) by A36, A100;
A106: ( 1 / 2 <= r1 & r1 <= 1 ) by A100, XXREAL_1:1;
then r1 * 2 >= (1 / 2) * 2 by XREAL_1:66;
then A107: (2 * r1) - 1 >= 0 by XREAL_1:50;
2 * 1 >= 2 * r1 by A106, XREAL_1:66;
then (1 + 1) - 1 >= (2 * r1) - 1 by XREAL_1:11;
then f3 . r1 in { (((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A105, A107;
then f3 . r2 in (LSeg |[a,c]|,|[a,d]|) /\ (LSeg |[a,d]|,|[b,d]|) by A87, A104, XBOOLE_0:def 4;
then A108: f3 . r2 = |[a,d]| by A88, TARSKI:def 1;
then (((1 - (2 * r2)) * |[a,c]|) + ((2 * r2) * |[a,d]|)) + (- |[a,d]|) = 0. (TOP-REAL 2) by A101, EUCLID:40;
then (((1 - (2 * r2)) * |[a,c]|) + ((2 * r2) * |[a,d]|)) + ((- 1) * |[a,d]|) = 0. (TOP-REAL 2) by EUCLID:43;
then ((1 - (2 * r2)) * |[a,c]|) + (((2 * r2) * |[a,d]|) + ((- 1) * |[a,d]|)) = 0. (TOP-REAL 2) by EUCLID:30;
then ((1 - (2 * r2)) * |[a,c]|) + (((2 * r2) + (- 1)) * |[a,d]|) = 0. (TOP-REAL 2) by EUCLID:37;
then ((1 - (2 * r2)) * |[a,c]|) + ((- (1 - (2 * r2))) * |[a,d]|) = 0. (TOP-REAL 2) ;
then ((1 - (2 * r2)) * |[a,c]|) + (- ((1 - (2 * r2)) * |[a,d]|)) = 0. (TOP-REAL 2) by EUCLID:44;
then ((1 - (2 * r2)) * |[a,c]|) - ((1 - (2 * r2)) * |[a,d]|) = 0. (TOP-REAL 2) by EUCLID:45;
then (1 - (2 * r2)) * (|[a,c]| - |[a,d]|) = 0. (TOP-REAL 2) by EUCLID:53;
then ( 1 - (2 * r2) = 0 or |[a,c]| - |[a,d]| = 0. (TOP-REAL 2) ) by EUCLID:35;
then ( 1 - (2 * r2) = 0 or |[a,c]| = |[a,d]| ) by EUCLID:47;
then A109: ( 1 - (2 * r2) = 0 or c = |[a,d]| `2 ) by EUCLID:56;
(((1 - ((2 * r1) - 1)) * |[a,d]|) + (((2 * r1) - 1) * |[b,d]|)) + (- |[a,d]|) = 0. (TOP-REAL 2) by A87, A105, A108, EUCLID:40;
then (((1 - ((2 * r1) - 1)) * |[a,d]|) + (((2 * r1) - 1) * |[b,d]|)) + ((- 1) * |[a,d]|) = 0. (TOP-REAL 2) by EUCLID:43;
then (((2 * r1) - 1) * |[b,d]|) + (((1 - ((2 * r1) - 1)) * |[a,d]|) + ((- 1) * |[a,d]|)) = 0. (TOP-REAL 2) by EUCLID:30;
then (((2 * r1) - 1) * |[b,d]|) + (((- 1) + (1 - ((2 * r1) - 1))) * |[a,d]|) = 0. (TOP-REAL 2) by EUCLID:37;
then (((2 * r1) - 1) * |[b,d]|) + ((- ((2 * r1) - 1)) * |[a,d]|) = 0. (TOP-REAL 2) ;
then (((2 * r1) - 1) * |[b,d]|) + (- (((2 * r1) - 1) * |[a,d]|)) = 0. (TOP-REAL 2) by EUCLID:44;
then (((2 * r1) - 1) * |[b,d]|) - (((2 * r1) - 1) * |[a,d]|) = 0. (TOP-REAL 2) by EUCLID:45;
then ((2 * r1) - 1) * (|[b,d]| - |[a,d]|) = 0. (TOP-REAL 2) by EUCLID:53;
then ( (2 * r1) - 1 = 0 or |[b,d]| - |[a,d]| = 0. (TOP-REAL 2) ) by EUCLID:35;
then ( (2 * r1) - 1 = 0 or |[b,d]| = |[a,d]| ) by EUCLID:47;
then ( (2 * r1) - 1 = 0 or b = |[a,d]| `1 ) by EUCLID:56;
hence x1 = x2 by A1, A109, EUCLID:56; :: thesis:

end;

case A110: ( x1 in [.(1 / 2),1.] & x2 in [.(1 / 2),1.] ) ; :: thesis:

then f3 . r1 = ((1 - ((2 * r1) - 1)) * |[a,d]|) + (((2 * r1) - 1) * |[b,d]|) by A36;
then ((1 - ((2 * r2) - 1)) * |[a,d]|) + (((2 * r2) - 1) * |[b,d]|) = ((1 - ((2 * r1) - 1)) * |[a,d]|) + (((2 * r1) - 1) * |[b,d]|) by A36, A87, A110;
then (((1 - ((2 * r2) - 1)) * |[a,d]|) + (((2 * r2) - 1) * |[b,d]|)) - (((2 * r1) - 1) * |[b,d]|) = (1 - ((2 * r1) - 1)) * |[a,d]| by EUCLID:52;
then ((1 - ((2 * r2) - 1)) * |[a,d]|) + ((((2 * r2) - 1) * |[b,d]|) - (((2 * r1) - 1) * |[b,d]|)) = (1 - ((2 * r1) - 1)) * |[a,d]| by EUCLID:49;
then ((1 - ((2 * r2) - 1)) * |[a,d]|) + ((((2 * r2) - 1) - ((2 * r1) - 1)) * |[b,d]|) = (1 - ((2 * r1) - 1)) * |[a,d]| by EUCLID:54;
then ((((2 * r2) - 1) - ((2 * r1) - 1)) * |[b,d]|) + (((1 - ((2 * r2) - 1)) * |[a,d]|) - ((1 - ((2 * r1) - 1)) * |[a,d]|)) = ((1 - ((2 * r1) - 1)) * |[a,d]|) - ((1 - ((2 * r1) - 1)) * |[a,d]|) by EUCLID:49;
then ((((2 * r2) - 1) - ((2 * r1) - 1)) * |[b,d]|) + (((1 - ((2 * r2) - 1)) * |[a,d]|) - ((1 - ((2 * r1) - 1)) * |[a,d]|)) = 0. (TOP-REAL 2) by EUCLID:46;
then ((((2 * r2) - 1) - ((2 * r1) - 1)) * |[b,d]|) + (((1 - ((2 * r2) - 1)) - (1 - ((2 * r1) - 1))) * |[a,d]|) = 0. (TOP-REAL 2) by EUCLID:54;
then ((((2 * r2) - 1) - ((2 * r1) - 1)) * |[b,d]|) + ((- (((2 * r2) - 1) - ((2 * r1) - 1))) * |[a,d]|) = 0. (TOP-REAL 2) ;
then ((((2 * r2) - 1) - ((2 * r1) - 1)) * |[b,d]|) + (- ((((2 * r2) - 1) - ((2 * r1) - 1)) * |[a,d]|)) = 0. (TOP-REAL 2) by EUCLID:44;
then ((((2 * r2) - 1) - ((2 * r1) - 1)) * |[b,d]|) - ((((2 * r2) - 1) - ((2 * r1) - 1)) * |[a,d]|) = 0. (TOP-REAL 2) by EUCLID:45;
then (((2 * r2) - 1) - ((2 * r1) - 1)) * (|[b,d]| - |[a,d]|) = 0. (TOP-REAL 2) by EUCLID:53;
then ( ((2 * r2) - 1) - ((2 * r1) - 1) = 0 or |[b,d]| - |[a,d]| = 0. (TOP-REAL 2) ) by EUCLID:35;
then ( ((2 * r2) - 1) - ((2 * r1) - 1) = 0 or |[b,d]| = |[a,d]| ) by EUCLID:47;
then ( ((2 * r2) - 1) - ((2 * r1) - 1) = 0 or b = |[a,d]| `1 ) by EUCLID:56;
hence x1 = x2 by A1, EUCLID:56; :: thesis:

end;

hence x1 = x2 ; :: thesis:

end;

then A111: f3 is one-to-one by FUNCT_1:def 8;
[#] ((TOP-REAL 2) | (Upper_Arc (rectangle a,b,c,d))) c= rng f3

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in [#] ((TOP-REAL 2) | (Upper_Arc (rectangle a,b,c,d))) ; :: thesis:
then A113: y in Upper_Arc (rectangle a,b,c,d) by PRE_TOPC:def 10;
then reconsider q = y as Point of (TOP-REAL 2) ;
A114: Upper_Arc (rectangle a,b,c,d) = (LSeg |[a,c]|,|[a,d]|) \/ (LSeg |[a,d]|,|[b,d]|) by A1, Th61;

now

per cases by A113, A114, XBOOLE_0:def 3;

case q in LSeg |[a,c]|,|[a,d]| ; :: thesis:

then A115: ( 0 <= (((q `2 ) - c) / (d - c)) / 2 & (((q `2 ) - c) / (d - c)) / 2 <= 1 & f3 . ((((q `2 ) - c) / (d - c)) / 2) = q ) by A38;
then (((q `2 ) - c) / (d - c)) / 2 in [.0 ,1.] by XXREAL_1:1;
hence y in rng f3 by A17, A115, FUNCT_1:def 5; :: thesis:

end;

case q in LSeg |[a,d]|,|[b,d]| ; :: thesis:

then A116: ( 0 <= ((((q `1 ) - a) / (b - a)) / 2) + (1 / 2) & ((((q `1 ) - a) / (b - a)) / 2) + (1 / 2) <= 1 & f3 . (((((q `1 ) - a) / (b - a)) / 2) + (1 / 2)) = q ) by A46;
then ((((q `1 ) - a) / (b - a)) / 2) + (1 / 2) in [.0 ,1.] by XXREAL_1:1;
hence y in rng f3 by A17, A116, FUNCT_1:def 5; :: thesis:

end;

hence y in rng f3 ; :: thesis:

end;

then A117: rng f3 = [#] ((TOP-REAL 2) | (Upper_Arc (rectangle a,b,c,d))) by XBOOLE_0:def 10;
A118: I[01] is compact by HEINE:11, TOPMETR:27;
A119: f3 is being_homeomorphism by A78, A85, A86, A111, A117, A118, COMPTS_1:26, JGRAPH_1:63;
rng f3 = Upper_Arc (rectangle a,b,c,d) by A117, PRE_TOPC:def 10;
hence ex f being Function of I[01] ,((TOP-REAL 2) | (Upper_Arc (rectangle a,b,c,d))) st
( f is being_homeomorphism & f . 0 = W-min (rectangle a,b,c,d) & f . 1 = E-max (rectangle a,b,c,d) & rng f = Upper_Arc (rectangle a,b,c,d) & ( for r being Real st r in [.0 ,(1 / 2).] holds
f . r = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) ) & ( for r being Real st r in [.(1 / 2),1.] holds
f . r = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) ) & ( for p being Point of (TOP-REAL 2) st p in LSeg |[a,c]|,|[a,d]| holds
( 0 <= (((p `2 ) - c) / (d - c)) / 2 & (((p `2 ) - c) / (d - c)) / 2 <= 1 & f . ((((p `2 ) - c) / (d - c)) / 2) = p ) ) & ( for p being Point of (TOP-REAL 2) st p in LSeg |[a,d]|,|[b,d]| holds
( 0 <= ((((p `1 ) - a) / (b - a)) / 2) + (1 / 2) & ((((p `1 ) - a) / (b - a)) / 2) + (1 / 2) <= 1 & f . (((((p `1 ) - a) / (b - a)) / 2) + (1 / 2)) = p ) ) ) by A30, A32, A33, A36, A38, A46, A119; :: thesis: