let a, b, c, d be Real; :: thesis: ( a < b & c < d implies 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 ) ) ) )
set K = rectangle (a,b,c,d);
assume that
A1: a < b and
A2: c < d ; :: thesis: 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 ) ) )
defpred S1[ object , object ] 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]|) ) );
A3: [.0,1.] = [.0,(1 / 2).] \/ [.(1 / 2),1.] by XXREAL_1:165;
A4: for x being object st x in [.0,1.] holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in [.0,1.] implies ex y being object st S1[x,y] )
assume A5: x in [.0,1.] ; :: thesis: ex y being object st S1[x,y]
now :: thesis: ( ( x in [.0,(1 / 2).] & ex y being object st S1[x,y] ) or ( x in [.(1 / 2),1.] & ex y being object st S1[x,y] ) )
per cases ( x in [.0,(1 / 2).] or x in [.(1 / 2),1.] ) by A3, A5, XBOOLE_0:def 3;
case A6: x in [.0,(1 / 2).] ; :: thesis: ex y being object st S1[x,y]
then reconsider r = x as Real ;
A7: r <= 1 / 2 by A6, 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: ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|)
then 1 / 2 <= r by XXREAL_1:1;
then A8: r = 1 / 2 by A7, XXREAL_0:1;
then A9: ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) = (0 * |[a,c]|) + |[a,d]| by RLVECT_1:def 8
.= (0. (TOP-REAL 2)) + |[a,d]| by RLVECT_1:10
.= |[a,d]| by RLVECT_1:4 ;
((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) = (1 * |[a,d]|) + (0. (TOP-REAL 2)) by A8, RLVECT_1:10
.= |[a,d]| + (0. (TOP-REAL 2)) by RLVECT_1:def 8
.= |[a,d]| by RLVECT_1:4 ;
hence ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) by A9; :: thesis: verum
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 object st S1[x,y] ; :: thesis: verum
end;
case A10: x in [.(1 / 2),1.] ; :: thesis: ex y being object st S1[x,y]
then reconsider r = x as Real ;
A11: 1 / 2 <= r by A10, 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: ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|)
then r <= 1 / 2 by XXREAL_1:1;
then A12: r = 1 / 2 by A11, XXREAL_0:1;
then A13: ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) = |[a,d]| + (0 * |[b,d]|) by RLVECT_1:def 8
.= |[a,d]| + (0. (TOP-REAL 2)) by RLVECT_1:10
.= |[a,d]| by RLVECT_1:4 ;
((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) = (0. (TOP-REAL 2)) + (1 * |[a,d]|) by A12, RLVECT_1:10
.= (0. (TOP-REAL 2)) + |[a,d]| by RLVECT_1:def 8
.= |[a,d]| by RLVECT_1:4 ;
hence ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) by A13; :: thesis: verum
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 object st S1[x,y] ; :: thesis: verum
end;
end;
end;
hence ex y being object st S1[x,y] ; :: thesis: verum
end;
ex f2 being Function st
( dom f2 = [.0,1.] & ( for x being object st x in [.0,1.] holds
S1[x,f2 . x] ) ) from CLASSES1:sch 1(A4);
 then consider f2 being Function such that
A14: dom f2 = [.0,1.] and
A15: for x being object st x in [.0,1.] holds
S1[x,f2 . x] ;
rng f2 c= the carrier of ((TOP-REAL 2) | (Upper_Arc (rectangle (a,b,c,d))))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f2 or y in the carrier of ((TOP-REAL 2) | (Upper_Arc (rectangle (a,b,c,d)))) )
assume y in rng f2 ; :: thesis: y in the carrier of ((TOP-REAL 2) | (Upper_Arc (rectangle (a,b,c,d))))
then consider x being object such that
A16: x in dom f2 and
A17: y = f2 . x by FUNCT_1:def 3;
now :: thesis: ( ( x in [.0,(1 / 2).] & y in the carrier of ((TOP-REAL 2) | (Upper_Arc (rectangle (a,b,c,d)))) ) or ( x in [.(1 / 2),1.] & y in the carrier of ((TOP-REAL 2) | (Upper_Arc (rectangle (a,b,c,d)))) ) )
per cases ( x in [.0,(1 / 2).] or x in [.(1 / 2),1.] ) by A3, A14, A16, XBOOLE_0:def 3;
case A18: x in [.0,(1 / 2).] ; :: thesis: y in the carrier of ((TOP-REAL 2) | (Upper_Arc (rectangle (a,b,c,d))))
then reconsider r = x as Real ;
A19: 0 <= r by A18, XXREAL_1:1;
r <= 1 / 2 by A18, XXREAL_1:1;
then A20: r * 2 <= (1 / 2) * 2 by XREAL_1:64;
f2 . x = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) by A14, A15, A16, A18;
then A21: y in { (((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A17, A19, A20;
Upper_Arc (rectangle (a,b,c,d)) = (LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|)) by A1, A2, Th51;
then y in Upper_Arc (rectangle (a,b,c,d)) by A21, XBOOLE_0:def 3;
hence y in the carrier of ((TOP-REAL 2) | (Upper_Arc (rectangle (a,b,c,d)))) by PRE_TOPC:8; :: thesis: verum
end;
case A22: x in [.(1 / 2),1.] ; :: thesis: y in the carrier of ((TOP-REAL 2) | (Upper_Arc (rectangle (a,b,c,d))))
then reconsider r = x as Real ;
A23: 1 / 2 <= r by A22, XXREAL_1:1;
A24: r <= 1 by A22, XXREAL_1:1;
r * 2 >= (1 / 2) * 2 by A23, XREAL_1:64;
then A25: (2 * r) - 1 >= 0 by XREAL_1:48;
2 * 1 >= 2 * r by A24, XREAL_1:64;
then A26: (1 + 1) - 1 >= (2 * r) - 1 by XREAL_1:9;
f2 . x = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) by A14, A15, A16, A22;
then A27: y in { (((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A17, A25, A26;
Upper_Arc (rectangle (a,b,c,d)) = (LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|)) by A1, A2, Th51;
then y in Upper_Arc (rectangle (a,b,c,d)) by A27, XBOOLE_0:def 3;
hence y in the carrier of ((TOP-REAL 2) | (Upper_Arc (rectangle (a,b,c,d)))) by PRE_TOPC:8; :: thesis: verum
end;
end;
end;
hence y in the carrier of ((TOP-REAL 2) | (Upper_Arc (rectangle (a,b,c,d)))) ; :: thesis: verum
end;
then reconsider f3 = f2 as Function of I[01],((TOP-REAL 2) | (Upper_Arc (rectangle (a,b,c,d)))) by A14, BORSUK_1:40, FUNCT_2:2;
A28: 0 in [.0,1.] by XXREAL_1:1;
0 in [.0,(1 / 2).] by XXREAL_1:1;
then A29: f3 . 0 = ((1 - (2 * 0)) * |[a,c]|) + ((2 * 0) * |[a,d]|) by A15, A28
.= (1 * |[a,c]|) + (0. (TOP-REAL 2)) by RLVECT_1:10
.= |[a,c]| + (0. (TOP-REAL 2)) by RLVECT_1:def 8
.= |[a,c]| by RLVECT_1:4
.= W-min (rectangle (a,b,c,d)) by A1, A2, Th46 ;
A30: 1 in [.0,1.] by XXREAL_1:1;
1 in [.(1 / 2),1.] by XXREAL_1:1;
then A31: f3 . 1 = ((1 - ((2 * 1) - 1)) * |[a,d]|) + (((2 * 1) - 1) * |[b,d]|) by A15, A30
.= (0 * |[a,d]|) + |[b,d]| by RLVECT_1:def 8
.= (0. (TOP-REAL 2)) + |[b,d]| by RLVECT_1:10
.= |[b,d]| by RLVECT_1:4
.= E-max (rectangle (a,b,c,d)) by A1, A2, Th46 ;
A32: 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: ( r in [.0,(1 / 2).] implies f3 . r = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) )
assume A33: r in [.0,(1 / 2).] ; :: thesis: f3 . r = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|)
then A34: 0 <= r by XXREAL_1:1;
r <= 1 / 2 by A33, XXREAL_1:1;
then r <= 1 by XXREAL_0:2;
then r in [.0,1.] by A34, XXREAL_1:1;
hence f3 . r = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) by A15, A33; :: thesis: verum
end;
A35: 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: ( r in [.(1 / 2),1.] implies f3 . r = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) )
assume A36: r in [.(1 / 2),1.] ; :: thesis: f3 . r = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|)
then A37: 1 / 2 <= r by XXREAL_1:1;
r <= 1 by A36, XXREAL_1:1;
then r in [.0,1.] by A37, XXREAL_1:1;
hence f3 . r = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) by A15, A36; :: thesis: verum
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: ( p in LSeg (|[a,c]|,|[a,d]|) implies ( 0 <= (((p `2) - c) / (d - c)) / 2 & (((p `2) - c) / (d - c)) / 2 <= 1 & f3 . ((((p `2) - c) / (d - c)) / 2) = p ) )
assume A39: p in LSeg (|[a,c]|,|[a,d]|) ; :: thesis: ( 0 <= (((p `2) - c) / (d - c)) / 2 & (((p `2) - c) / (d - c)) / 2 <= 1 & f3 . ((((p `2) - c) / (d - c)) / 2) = p )
A40: |[a,c]| `2 = c by EUCLID:52;
A41: |[a,d]| `2 = d by EUCLID:52;
then A42: c <= p `2 by A2, A39, A40, TOPREAL1:4;
A43: p `2 <= d by A2, A39, A40, A41, TOPREAL1:4;
A44: d - c > 0 by A2, XREAL_1:50;
A45: (p `2) - c >= 0 by A42, XREAL_1:48;
A46: d - c > 0 by A2, XREAL_1:50;
(p `2) - c <= d - c by A43, XREAL_1:9;
then ((p `2) - c) / (d - c) <= (d - c) / (d - c) by A46, XREAL_1:72;
then ((p `2) - c) / (d - c) <= 1 by A46, XCMPLX_1:60;
then A47: (((p `2) - c) / (d - c)) / 2 <= 1 / 2 by XREAL_1:72;
set r = (((p `2) - c) / (d - c)) / 2;
(((p `2) - c) / (d - c)) / 2 in [.0,(1 / 2).] by A44, A45, A47, 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 A32
.= |[((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:58
.= |[((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:58
.= |[(((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:56
.= |[a,((1 * c) + ((((p `2) - c) / (d - c)) * (d - c)))]|
.= |[a,((1 * c) + ((p `2) - c))]| by A46, XCMPLX_1:87
.= |[(p `1),(p `2)]| by A39, TOPREAL3:11
.= p by EUCLID:53 ;
hence ( 0 <= (((p `2) - c) / (d - c)) / 2 & (((p `2) - c) / (d - c)) / 2 <= 1 & f3 . ((((p `2) - c) / (d - c)) / 2) = p ) by A44, A45, A47, XXREAL_0:2; :: thesis: verum
end;
A48: 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: ( p in LSeg (|[a,d]|,|[b,d]|) implies ( 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 ) )
assume A49: p in LSeg (|[a,d]|,|[b,d]|) ; :: thesis: ( 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 )
A50: |[a,d]| `1 = a by EUCLID:52;
A51: |[b,d]| `1 = b by EUCLID:52;
then A52: a <= p `1 by A1, A49, A50, TOPREAL1:3;
A53: p `1 <= b by A1, A49, A50, A51, TOPREAL1:3;
A54: b - a > 0 by A1, XREAL_1:50;
A55: (p `1) - a >= 0 by A52, XREAL_1:48;
then A56: ((((p `1) - a) / (b - a)) / 2) + (1 / 2) >= 0 + (1 / 2) by A54, XREAL_1:7;
A57: b - a > 0 by A1, XREAL_1:50;
(p `1) - a <= b - a by A53, XREAL_1:9;
then ((p `1) - a) / (b - a) <= (b - a) / (b - a) by A57, XREAL_1:72;
then ((p `1) - a) / (b - a) <= 1 by A57, XCMPLX_1:60;
then (((p `1) - a) / (b - a)) / 2 <= 1 / 2 by XREAL_1:72;
then A58: ((((p `1) - a) / (b - a)) / 2) + (1 / 2) <= (1 / 2) + (1 / 2) by XREAL_1:7;
set r = ((((p `1) - a) / (b - a)) / 2) + (1 / 2);
((((p `1) - a) / (b - a)) / 2) + (1 / 2) in [.(1 / 2),1.] by A56, A58, 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 A35
.= |[((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:58
.= |[((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:58
.= |[(((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:56
.= |[((1 * a) + ((((p `1) - a) / (b - a)) * (b - a))),d]|
.= |[((1 * a) + ((p `1) - a)),d]| by A57, XCMPLX_1:87
.= |[(p `1),(p `2)]| by A49, TOPREAL3:12
.= p by EUCLID:53 ;
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 A54, A55, A58; :: thesis: verum
end;
reconsider B00 = [.0,1.] as Subset of R^1 by TOPMETR:17;
reconsider B01 = B00 as non empty Subset of R^1 by XXREAL_1:1;
I[01] = R^1 | B01 by TOPMETR:19, TOPMETR:20;
then consider h1 being Function of I[01],R^1 such that
A59: for p being Point of I[01] holds h1 . p = p and
A60: h1 is continuous by Th6;
consider h2 being Function of I[01],R^1 such that
A61: for p being Point of I[01]
for r1 being Real st h1 . p = r1 holds
h2 . p = 2 * r1 and
A62: h2 is continuous by A60, JGRAPH_2:23;
consider h5 being Function of I[01],R^1 such that
A63: for p being Point of I[01]
for r1 being Real st h2 . p = r1 holds
h5 . p = 1 - r1 and
A64: h5 is continuous by A62, Th8;
consider h3 being Function of I[01],R^1 such that
A65: for p being Point of I[01]
for r1 being Real st h2 . p = r1 holds
h3 . p = r1 - 1 and
A66: h3 is continuous by A62, Th7;
consider h4 being Function of I[01],R^1 such that
A67: for p being Point of I[01]
for r1 being Real st h3 . p = r1 holds
h4 . p = 1 - r1 and
A68: h4 is continuous by A66, Th8;
consider g1 being Function of I[01],(TOP-REAL 2) such that
A69: for r being Point of I[01] holds g1 . r = ((h5 . r) * |[a,c]|) + ((h2 . r) * |[a,d]|) and
A70: g1 is continuous by A62, A64, Th13;
A71: for r being Point of I[01]
for s being Real st r = s holds
g1 . r = ((1 - (2 * s)) * |[a,c]|) + ((2 * s) * |[a,d]|)
proof
let r be Point of I[01]; :: thesis: for s being Real st r = s holds
g1 . r = ((1 - (2 * s)) * |[a,c]|) + ((2 * s) * |[a,d]|)
let s be Real; :: thesis: ( r = s implies g1 . r = ((1 - (2 * s)) * |[a,c]|) + ((2 * s) * |[a,d]|) )
assume A72: r = s ; :: thesis: g1 . r = ((1 - (2 * s)) * |[a,c]|) + ((2 * s) * |[a,d]|)
g1 . r = ((h5 . r) * |[a,c]|) + ((h2 . r) * |[a,d]|) by A69
.= ((1 - (2 * (h1 . r))) * |[a,c]|) + ((h2 . r) * |[a,d]|) by A61, A63
.= ((1 - (2 * (h1 . r))) * |[a,c]|) + ((2 * (h1 . r)) * |[a,d]|) by A61
.= ((1 - (2 * s)) * |[a,c]|) + ((2 * (h1 . r)) * |[a,d]|) by A59, A72
.= ((1 - (2 * s)) * |[a,c]|) + ((2 * s) * |[a,d]|) by A59, A72 ;
hence g1 . r = ((1 - (2 * s)) * |[a,c]|) + ((2 * s) * |[a,d]|) ; :: thesis: verum
end;
consider g2 being Function of I[01],(TOP-REAL 2) such that
A73: for r being Point of I[01] holds g2 . r = ((h4 . r) * |[a,d]|) + ((h3 . r) * |[b,d]|) and
A74: g2 is continuous by A66, A68, Th13;
A75: for r being Point of I[01]
for s being Real 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: for s being Real st r = s holds
g2 . r = ((1 - ((2 * s) - 1)) * |[a,d]|) + (((2 * s) - 1) * |[b,d]|)
let s be Real; :: thesis: ( r = s implies g2 . r = ((1 - ((2 * s) - 1)) * |[a,d]|) + (((2 * s) - 1) * |[b,d]|) )
assume A76: r = s ; :: thesis: g2 . r = ((1 - ((2 * s) - 1)) * |[a,d]|) + (((2 * s) - 1) * |[b,d]|)
g2 . r = ((h4 . r) * |[a,d]|) + ((h3 . r) * |[b,d]|) by A73
.= ((1 - ((h2 . r) - 1)) * |[a,d]|) + ((h3 . r) * |[b,d]|) by A65, A67
.= ((1 - ((h2 . r) - 1)) * |[a,d]|) + (((h2 . r) - 1) * |[b,d]|) by A65
.= ((1 - ((2 * (h1 . r)) - 1)) * |[a,d]|) + (((h2 . r) - 1) * |[b,d]|) by A61
.= ((1 - ((2 * (h1 . r)) - 1)) * |[a,d]|) + (((2 * (h1 . r)) - 1) * |[b,d]|) by A61
.= ((1 - ((2 * s) - 1)) * |[a,d]|) + (((2 * (h1 . r)) - 1) * |[b,d]|) by A59, A76
.= ((1 - ((2 * s) - 1)) * |[a,d]|) + (((2 * s) - 1) * |[b,d]|) by A59, A76 ;
hence g2 . r = ((1 - ((2 * s) - 1)) * |[a,d]|) + (((2 * s) - 1) * |[b,d]|) ; :: thesis: verum
end;
reconsider B11 = [.0,(1 / 2).] as non empty Subset of I[01] by A3, BORSUK_1:40, XBOOLE_1:7, XXREAL_1:1;
A77: dom (g1 | B11) = (dom g1) /\ B11 by RELAT_1:61
.= 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:8 ;
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 A77, FUNCT_2:2;
A78: TOP-REAL 2 is SubSpace of TOP-REAL 2 by TSEP_1:2;
then A79: g11 is continuous by A70, BORSUK_4:44;
reconsider B22 = [.(1 / 2),1.] as non empty Subset of I[01] by A3, BORSUK_1:40, XBOOLE_1:7, XXREAL_1:1;
A80: dom (g2 | B22) = (dom g2) /\ B22 by RELAT_1:61
.= 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:8 ;
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 A80, FUNCT_2:2;
A81: g22 is continuous by A74, A78, BORSUK_4:44;
A82: B11 = [#] (I[01] | B11) by PRE_TOPC:def 5;
A83: B22 = [#] (I[01] | B22) by PRE_TOPC:def 5;
A84: B11 is closed by Th4;
A85: B22 is closed by Th4;
A86: ([#] (I[01] | B11)) \/ ([#] (I[01] | B22)) = [#] I[01] by A82, A83, BORSUK_1:40, XXREAL_1:165;
for p being object st p in ([#] (I[01] | B11)) /\ ([#] (I[01] | B22)) holds
g11 . p = g22 . p
proof
let p be object ; :: thesis: ( p in ([#] (I[01] | B11)) /\ ([#] (I[01] | B22)) implies g11 . p = g22 . p )
assume A87: p in ([#] (I[01] | B11)) /\ ([#] (I[01] | B22)) ; :: thesis: g11 . p = g22 . p
then A88: p in [#] (I[01] | B11) by XBOOLE_0:def 4;
A89: p in [#] (I[01] | B22) by A87;
A90: p in B11 by A88, PRE_TOPC:def 5;
A91: p in B22 by A89, PRE_TOPC:def 5;
reconsider rp = p as Real by A90;
A92: rp <= 1 / 2 by A90, XXREAL_1:1;
rp >= 1 / 2 by A91, XXREAL_1:1;
then rp = 1 / 2 by A92, XXREAL_0:1;
then A93: 2 * rp = 1 ;
thus g11 . p = g1 . p by A90, FUNCT_1:49
.= ((1 - 1) * |[a,c]|) + (1 * |[a,d]|) by A71, A90, A93
.= (0. (TOP-REAL 2)) + (1 * |[a,d]|) by RLVECT_1:10
.= ((1 - 0) * |[a,d]|) + ((1 - 1) * |[b,d]|) by RLVECT_1:10
.= g2 . p by A75, A90, A93
.= g22 . p by A91, FUNCT_1:49 ; :: thesis: verum
end;
then consider h being Function of I[01],(TOP-REAL 2) such that
A94: h = g11 +* g22 and
A95: h is continuous by A79, A81, A82, A83, A84, A85, A86, JGRAPH_2:1;
A96: dom f3 = dom h by Th5;
A97: dom f3 = the carrier of I[01] by Th5;
for x being object st x in dom f2 holds
f3 . x = h . x
proof
let x be object ; :: thesis: ( x in dom f2 implies f3 . x = h . x )
assume A98: x in dom f2 ; :: thesis: f3 . x = h . x
then reconsider rx = x as Real by A97;
A99: 0 <= rx by A96, A98, BORSUK_1:40, XXREAL_1:1;
A100: rx <= 1 by A96, A98, BORSUK_1:40, XXREAL_1:1;
now :: thesis: ( ( rx < 1 / 2 & f3 . x = h . x ) or ( rx >= 1 / 2 & f3 . x = h . x ) )
per cases ( rx < 1 / 2 or rx >= 1 / 2 ) ;
case A101: rx < 1 / 2 ; :: thesis: f3 . x = h . x
then A102: rx in [.0,(1 / 2).] by A99, XXREAL_1:1;
not rx in dom g22 by A83, A101, XXREAL_1:1;
then h . rx = g11 . rx by A94, FUNCT_4:11
.= g1 . rx by A102, FUNCT_1:49
.= ((1 - (2 * rx)) * |[a,c]|) + ((2 * rx) * |[a,d]|) by A71, A96, A98
.= f3 . rx by A32, A102 ;
hence f3 . x = h . x ; :: thesis: verum
end;
case rx >= 1 / 2 ; :: thesis: f3 . x = h . x
then A103: rx in [.(1 / 2),1.] by A100, XXREAL_1:1;
then rx in [#] (I[01] | B22) by PRE_TOPC:def 5;
then h . rx = g22 . rx by A80, A94, FUNCT_4:13
.= g2 . rx by A103, FUNCT_1:49
.= ((1 - ((2 * rx) - 1)) * |[a,d]|) + (((2 * rx) - 1) * |[b,d]|) by A75, A96, A98
.= f3 . rx by A35, A103 ;
hence f3 . x = h . x ; :: thesis: verum
end;
end;
end;
hence f3 . x = h . x ; :: thesis: verum
end;
then A104: f2 = h by A96, FUNCT_1:2;
for x1, x2 being object st x1 in dom f3 & x2 in dom f3 & f3 . x1 = f3 . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in dom f3 & x2 in dom f3 & f3 . x1 = f3 . x2 implies x1 = x2 )
assume that
A105: x1 in dom f3 and
A106: x2 in dom f3 and
A107: f3 . x1 = f3 . x2 ; :: thesis: x1 = x2
reconsider r1 = x1 as Real by A105;
reconsider r2 = x2 as Real by A106;
A108: (LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,d]|,|[b,d]|)) = {|[a,d]|} by A1, A2, Th34;
now :: thesis: ( ( x1 in [.0,(1 / 2).] & x2 in [.0,(1 / 2).] & x1 = x2 ) or ( x1 in [.0,(1 / 2).] & x2 in [.(1 / 2),1.] & x1 = x2 ) or ( x1 in [.(1 / 2),1.] & x2 in [.0,(1 / 2).] & x1 = x2 ) or ( x1 in [.(1 / 2),1.] & x2 in [.(1 / 2),1.] & x1 = x2 ) )
per cases ( ( x1 in [.0,(1 / 2).] & x2 in [.0,(1 / 2).] ) or ( x1 in [.0,(1 / 2).] & x2 in [.(1 / 2),1.] ) or ( x1 in [.(1 / 2),1.] & x2 in [.0,(1 / 2).] ) or ( x1 in [.(1 / 2),1.] & x2 in [.(1 / 2),1.] ) ) by A3, A14, A105, A106, XBOOLE_0:def 3;
case A109: ( x1 in [.0,(1 / 2).] & x2 in [.0,(1 / 2).] ) ; :: thesis: x1 = x2
then f3 . r1 = ((1 - (2 * r1)) * |[a,c]|) + ((2 * r1) * |[a,d]|) by A32;
then ((1 - (2 * r2)) * |[a,c]|) + ((2 * r2) * |[a,d]|) = ((1 - (2 * r1)) * |[a,c]|) + ((2 * r1) * |[a,d]|) by A32, A107, A109;
then (((1 - (2 * r2)) * |[a,c]|) + ((2 * r2) * |[a,d]|)) - ((2 * r1) * |[a,d]|) = (1 - (2 * r1)) * |[a,c]| by RLVECT_4:1;
then ((1 - (2 * r2)) * |[a,c]|) + (((2 * r2) * |[a,d]|) - ((2 * r1) * |[a,d]|)) = (1 - (2 * r1)) * |[a,c]| by RLVECT_1:def 3;
then ((1 - (2 * r2)) * |[a,c]|) + (((2 * r2) - (2 * r1)) * |[a,d]|) = (1 - (2 * r1)) * |[a,c]| by RLVECT_1:35;
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 RLVECT_1:def 3;
then (((2 * r2) - (2 * r1)) * |[a,d]|) + (((1 - (2 * r2)) * |[a,c]|) - ((1 - (2 * r1)) * |[a,c]|)) = 0. (TOP-REAL 2) by RLVECT_1:5;
then (((2 * r2) - (2 * r1)) * |[a,d]|) + (((1 - (2 * r2)) - (1 - (2 * r1))) * |[a,c]|) = 0. (TOP-REAL 2) by RLVECT_1:35;
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 RLVECT_1:79;
then (((2 * r2) - (2 * r1)) * |[a,d]|) - (((2 * r2) - (2 * r1)) * |[a,c]|) = 0. (TOP-REAL 2) ;
then ((2 * r2) - (2 * r1)) * (|[a,d]| - |[a,c]|) = 0. (TOP-REAL 2) by RLVECT_1:34;
then ( (2 * r2) - (2 * r1) = 0 or |[a,d]| - |[a,c]| = 0. (TOP-REAL 2) ) by RLVECT_1:11;
then ( (2 * r2) - (2 * r1) = 0 or |[a,d]| = |[a,c]| ) by RLVECT_1:21;
then ( (2 * r2) - (2 * r1) = 0 or d = |[a,c]| `2 ) by EUCLID:52;
hence x1 = x2 by A2, EUCLID:52; :: thesis: verum
end;
case A110: ( x1 in [.0,(1 / 2).] & x2 in [.(1 / 2),1.] ) ; :: thesis: x1 = x2
then A111: f3 . r1 = ((1 - (2 * r1)) * |[a,c]|) + ((2 * r1) * |[a,d]|) by A32;
A112: 0 <= r1 by A110, XXREAL_1:1;
r1 <= 1 / 2 by A110, XXREAL_1:1;
then r1 * 2 <= (1 / 2) * 2 by XREAL_1:64;
then A113: f3 . r1 in LSeg (|[a,c]|,|[a,d]|) by A111, A112;
A114: f3 . r2 = ((1 - ((2 * r2) - 1)) * |[a,d]|) + (((2 * r2) - 1) * |[b,d]|) by A35, A110;
A115: 1 / 2 <= r2 by A110, XXREAL_1:1;
A116: r2 <= 1 by A110, XXREAL_1:1;
r2 * 2 >= (1 / 2) * 2 by A115, XREAL_1:64;
then A117: (2 * r2) - 1 >= 0 by XREAL_1:48;
2 * 1 >= 2 * r2 by A116, XREAL_1:64;
then (1 + 1) - 1 >= (2 * r2) - 1 by XREAL_1:9;
then f3 . r2 in { (((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A114, A117;
then f3 . r1 in (LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,d]|,|[b,d]|)) by A107, A113, XBOOLE_0:def 4;
then A118: f3 . r1 = |[a,d]| by A108, TARSKI:def 1;
then (((1 - (2 * r1)) * |[a,c]|) + ((2 * r1) * |[a,d]|)) + (- |[a,d]|) = 0. (TOP-REAL 2) by A111, RLVECT_1:5;
then (((1 - (2 * r1)) * |[a,c]|) + ((2 * r1) * |[a,d]|)) + ((- 1) * |[a,d]|) = 0. (TOP-REAL 2) by RLVECT_1:16;
then ((1 - (2 * r1)) * |[a,c]|) + (((2 * r1) * |[a,d]|) + ((- 1) * |[a,d]|)) = 0. (TOP-REAL 2) by RLVECT_1:def 3;
then ((1 - (2 * r1)) * |[a,c]|) + (((2 * r1) + (- 1)) * |[a,d]|) = 0. (TOP-REAL 2) by RLVECT_1:def 6;
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 RLVECT_1:79;
then ((1 - (2 * r1)) * |[a,c]|) - ((1 - (2 * r1)) * |[a,d]|) = 0. (TOP-REAL 2) ;
then (1 - (2 * r1)) * (|[a,c]| - |[a,d]|) = 0. (TOP-REAL 2) by RLVECT_1:34;
then ( 1 - (2 * r1) = 0 or |[a,c]| - |[a,d]| = 0. (TOP-REAL 2) ) by RLVECT_1:11;
then ( 1 - (2 * r1) = 0 or |[a,c]| = |[a,d]| ) by RLVECT_1:21;
then A119: ( 1 - (2 * r1) = 0 or c = |[a,d]| `2 ) by EUCLID:52;
(((1 - ((2 * r2) - 1)) * |[a,d]|) + (((2 * r2) - 1) * |[b,d]|)) + (- |[a,d]|) = 0. (TOP-REAL 2) by A107, A114, A118, RLVECT_1:5;
then (((1 - ((2 * r2) - 1)) * |[a,d]|) + (((2 * r2) - 1) * |[b,d]|)) + ((- 1) * |[a,d]|) = 0. (TOP-REAL 2) by RLVECT_1:16;
then (((2 * r2) - 1) * |[b,d]|) + (((1 - ((2 * r2) - 1)) * |[a,d]|) + ((- 1) * |[a,d]|)) = 0. (TOP-REAL 2) by RLVECT_1:def 3;
then (((2 * r2) - 1) * |[b,d]|) + (((1 - ((2 * r2) - 1)) + (- 1)) * |[a,d]|) = 0. (TOP-REAL 2) by RLVECT_1:def 6;
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 RLVECT_1:79;
then (((2 * r2) - 1) * |[b,d]|) - (((2 * r2) - 1) * |[a,d]|) = 0. (TOP-REAL 2) ;
then ((2 * r2) - 1) * (|[b,d]| - |[a,d]|) = 0. (TOP-REAL 2) by RLVECT_1:34;
then ( (2 * r2) - 1 = 0 or |[b,d]| - |[a,d]| = 0. (TOP-REAL 2) ) by RLVECT_1:11;
then ( (2 * r2) - 1 = 0 or |[b,d]| = |[a,d]| ) by RLVECT_1:21;
then ( (2 * r2) - 1 = 0 or b = |[a,d]| `1 ) by EUCLID:52;
hence x1 = x2 by A1, A2, A119, EUCLID:52; :: thesis: verum
end;
case A120: ( x1 in [.(1 / 2),1.] & x2 in [.0,(1 / 2).] ) ; :: thesis: x1 = x2
then A121: f3 . r2 = ((1 - (2 * r2)) * |[a,c]|) + ((2 * r2) * |[a,d]|) by A32;
A122: 0 <= r2 by A120, XXREAL_1:1;
r2 <= 1 / 2 by A120, XXREAL_1:1;
then r2 * 2 <= (1 / 2) * 2 by XREAL_1:64;
then A123: f3 . r2 in LSeg (|[a,c]|,|[a,d]|) by A121, A122;
A124: f3 . r1 = ((1 - ((2 * r1) - 1)) * |[a,d]|) + (((2 * r1) - 1) * |[b,d]|) by A35, A120;
A125: 1 / 2 <= r1 by A120, XXREAL_1:1;
A126: r1 <= 1 by A120, XXREAL_1:1;
r1 * 2 >= (1 / 2) * 2 by A125, XREAL_1:64;
then A127: (2 * r1) - 1 >= 0 by XREAL_1:48;
2 * 1 >= 2 * r1 by A126, XREAL_1:64;
then (1 + 1) - 1 >= (2 * r1) - 1 by XREAL_1:9;
then f3 . r1 in { (((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A124, A127;
then f3 . r2 in (LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,d]|,|[b,d]|)) by A107, A123, XBOOLE_0:def 4;
then A128: f3 . r2 = |[a,d]| by A108, TARSKI:def 1;
then (((1 - (2 * r2)) * |[a,c]|) + ((2 * r2) * |[a,d]|)) + (- |[a,d]|) = 0. (TOP-REAL 2) by A121, RLVECT_1:5;
then (((1 - (2 * r2)) * |[a,c]|) + ((2 * r2) * |[a,d]|)) + ((- 1) * |[a,d]|) = 0. (TOP-REAL 2) by RLVECT_1:16;
then ((1 - (2 * r2)) * |[a,c]|) + (((2 * r2) * |[a,d]|) + ((- 1) * |[a,d]|)) = 0. (TOP-REAL 2) by RLVECT_1:def 3;
then ((1 - (2 * r2)) * |[a,c]|) + (((2 * r2) + (- 1)) * |[a,d]|) = 0. (TOP-REAL 2) by RLVECT_1:def 6;
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 RLVECT_1:79;
then ((1 - (2 * r2)) * |[a,c]|) - ((1 - (2 * r2)) * |[a,d]|) = 0. (TOP-REAL 2) ;
then (1 - (2 * r2)) * (|[a,c]| - |[a,d]|) = 0. (TOP-REAL 2) by RLVECT_1:34;
then ( 1 - (2 * r2) = 0 or |[a,c]| - |[a,d]| = 0. (TOP-REAL 2) ) by RLVECT_1:11;
then ( 1 - (2 * r2) = 0 or |[a,c]| = |[a,d]| ) by RLVECT_1:21;
then A129: ( 1 - (2 * r2) = 0 or c = |[a,d]| `2 ) by EUCLID:52;
(((1 - ((2 * r1) - 1)) * |[a,d]|) + (((2 * r1) - 1) * |[b,d]|)) + (- |[a,d]|) = 0. (TOP-REAL 2) by A107, A124, A128, RLVECT_1:5;
then (((1 - ((2 * r1) - 1)) * |[a,d]|) + (((2 * r1) - 1) * |[b,d]|)) + ((- 1) * |[a,d]|) = 0. (TOP-REAL 2) by RLVECT_1:16;
then (((2 * r1) - 1) * |[b,d]|) + (((1 - ((2 * r1) - 1)) * |[a,d]|) + ((- 1) * |[a,d]|)) = 0. (TOP-REAL 2) by RLVECT_1:def 3;
then (((2 * r1) - 1) * |[b,d]|) + (((- 1) + (1 - ((2 * r1) - 1))) * |[a,d]|) = 0. (TOP-REAL 2) by RLVECT_1:def 6;
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 RLVECT_1:79;
then (((2 * r1) - 1) * |[b,d]|) - (((2 * r1) - 1) * |[a,d]|) = 0. (TOP-REAL 2) ;
then ((2 * r1) - 1) * (|[b,d]| - |[a,d]|) = 0. (TOP-REAL 2) by RLVECT_1:34;
then ( (2 * r1) - 1 = 0 or |[b,d]| - |[a,d]| = 0. (TOP-REAL 2) ) by RLVECT_1:11;
then ( (2 * r1) - 1 = 0 or |[b,d]| = |[a,d]| ) by RLVECT_1:21;
then ( (2 * r1) - 1 = 0 or b = |[a,d]| `1 ) by EUCLID:52;
hence x1 = x2 by A1, A2, A129, EUCLID:52; :: thesis: verum
end;
case A130: ( x1 in [.(1 / 2),1.] & x2 in [.(1 / 2),1.] ) ; :: thesis: x1 = x2
then f3 . r1 = ((1 - ((2 * r1) - 1)) * |[a,d]|) + (((2 * r1) - 1) * |[b,d]|) by A35;
then ((1 - ((2 * r2) - 1)) * |[a,d]|) + (((2 * r2) - 1) * |[b,d]|) = ((1 - ((2 * r1) - 1)) * |[a,d]|) + (((2 * r1) - 1) * |[b,d]|) by A35, A107, A130;
then (((1 - ((2 * r2) - 1)) * |[a,d]|) + (((2 * r2) - 1) * |[b,d]|)) - (((2 * r1) - 1) * |[b,d]|) = (1 - ((2 * r1) - 1)) * |[a,d]| by RLVECT_4:1;
then ((1 - ((2 * r2) - 1)) * |[a,d]|) + ((((2 * r2) - 1) * |[b,d]|) - (((2 * r1) - 1) * |[b,d]|)) = (1 - ((2 * r1) - 1)) * |[a,d]| by RLVECT_1:def 3;
then ((1 - ((2 * r2) - 1)) * |[a,d]|) + ((((2 * r2) - 1) - ((2 * r1) - 1)) * |[b,d]|) = (1 - ((2 * r1) - 1)) * |[a,d]| by RLVECT_1:35;
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 RLVECT_1:def 3;
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 RLVECT_1:5;
then ((((2 * r2) - 1) - ((2 * r1) - 1)) * |[b,d]|) + (((1 - ((2 * r2) - 1)) - (1 - ((2 * r1) - 1))) * |[a,d]|) = 0. (TOP-REAL 2) by RLVECT_1:35;
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 RLVECT_1:79;
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]| - |[a,d]|) = 0. (TOP-REAL 2) by RLVECT_1:34;
then ( ((2 * r2) - 1) - ((2 * r1) - 1) = 0 or |[b,d]| - |[a,d]| = 0. (TOP-REAL 2) ) by RLVECT_1:11;
then ( ((2 * r2) - 1) - ((2 * r1) - 1) = 0 or |[b,d]| = |[a,d]| ) by RLVECT_1:21;
then ( ((2 * r2) - 1) - ((2 * r1) - 1) = 0 or b = |[a,d]| `1 ) by EUCLID:52;
hence x1 = x2 by A1, EUCLID:52; :: thesis: verum
end;
end;
end;
hence x1 = x2 ; :: thesis: verum
end;
then A131: f3 is one-to-one by FUNCT_1:def 4;
[#] ((TOP-REAL 2) | (Upper_Arc (rectangle (a,b,c,d)))) c= rng f3
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [#] ((TOP-REAL 2) | (Upper_Arc (rectangle (a,b,c,d)))) or y in rng f3 )
assume y in [#] ((TOP-REAL 2) | (Upper_Arc (rectangle (a,b,c,d)))) ; :: thesis: y in rng f3
then A132: y in Upper_Arc (rectangle (a,b,c,d)) by PRE_TOPC:def 5;
then reconsider q = y as Point of (TOP-REAL 2) ;
A133: Upper_Arc (rectangle (a,b,c,d)) = (LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|)) by A1, A2, Th51;
now :: thesis: ( ( q in LSeg (|[a,c]|,|[a,d]|) & y in rng f3 ) or ( q in LSeg (|[a,d]|,|[b,d]|) & y in rng f3 ) )
per cases ( q in LSeg (|[a,c]|,|[a,d]|) or q in LSeg (|[a,d]|,|[b,d]|) ) by A132, A133, XBOOLE_0:def 3;
case A134: q in LSeg (|[a,c]|,|[a,d]|) ; :: thesis: y in rng f3
then A135: 0 <= (((q `2) - c) / (d - c)) / 2 by A38;
A136: (((q `2) - c) / (d - c)) / 2 <= 1 by A38, A134;
A137: f3 . ((((q `2) - c) / (d - c)) / 2) = q by A38, A134;
(((q `2) - c) / (d - c)) / 2 in [.0,1.] by A135, A136, XXREAL_1:1;
hence y in rng f3 by A14, A137, FUNCT_1:def 3; :: thesis: verum
end;
case A138: q in LSeg (|[a,d]|,|[b,d]|) ; :: thesis: y in rng f3
then A139: 0 <= ((((q `1) - a) / (b - a)) / 2) + (1 / 2) by A48;
A140: ((((q `1) - a) / (b - a)) / 2) + (1 / 2) <= 1 by A48, A138;
A141: f3 . (((((q `1) - a) / (b - a)) / 2) + (1 / 2)) = q by A48, A138;
((((q `1) - a) / (b - a)) / 2) + (1 / 2) in [.0,1.] by A139, A140, XXREAL_1:1;
hence y in rng f3 by A14, A141, FUNCT_1:def 3; :: thesis: verum
end;
end;
end;
hence y in rng f3 ; :: thesis: verum
end;
then A142: rng f3 = [#] ((TOP-REAL 2) | (Upper_Arc (rectangle (a,b,c,d)))) ;
I[01] is compact by HEINE:4, TOPMETR:20;
then A143: f3 is being_homeomorphism by A95, A104, A131, A142, COMPTS_1:17, JGRAPH_1:45;
rng f3 = Upper_Arc (rectangle (a,b,c,d)) by A142, PRE_TOPC:def 5;
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 A29, A31, A32, A35, A38, A48, A143; :: thesis: verum