let f be FinSequence of (TOP-REAL 2); :: thesis: for p, q being Point of (TOP-REAL 2)
for r being Real st 0 <= r & r <= 1 & <*p,q*> is_in_the_area_of f holds
<*(((1 - r) * p) + (r * q))*> is_in_the_area_of f
let p, q be Point of (TOP-REAL 2); :: thesis: for r being Real st 0 <= r & r <= 1 & <*p,q*> is_in_the_area_of f holds
<*(((1 - r) * p) + (r * q))*> is_in_the_area_of f
let r be Real; :: thesis: ( 0 <= r & r <= 1 & <*p,q*> is_in_the_area_of f implies <*(((1 - r) * p) + (r * q))*> is_in_the_area_of f )
assume that
A1: 0 <= r and
A2: r <= 1 and
A3: <*p,q*> is_in_the_area_of f ; :: thesis: <*(((1 - r) * p) + (r * q))*> is_in_the_area_of f
dom <*p,q*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
then ( 1 in dom <*p,q*> & <*p,q*> /. 1 = p & 2 in dom <*p,q*> & <*p,q*> /. 2 = q ) by FINSEQ_4:26, TARSKI:def 2;
then A4: ( W-bound (L~ f) <= p `1 & p `1 <= E-bound (L~ f) & S-bound (L~ f) <= p `2 & p `2 <= N-bound (L~ f) & W-bound (L~ f) <= q `1 & q `1 <= E-bound (L~ f) & S-bound (L~ f) <= q `2 & q `2 <= N-bound (L~ f) ) by A3, SPRECT_2:def 1;
let n be Element of NAT ; :: according to SPRECT_2:def 1 :: thesis: ( not n in dom <*(((1 - r) * p) + (r * q))*> or ( W-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `1 & (<*(((1 - r) * p) + (r * q))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `2 & (<*(((1 - r) * p) + (r * q))*> /. n) `2 <= N-bound (L~ f) ) )
assume A5: n in dom <*(((1 - r) * p) + (r * q))*> ; :: thesis: ( W-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `1 & (<*(((1 - r) * p) + (r * q))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `2 & (<*(((1 - r) * p) + (r * q))*> /. n) `2 <= N-bound (L~ f) )
dom <*(((1 - r) * p) + (r * q))*> = {1} by FINSEQ_1:4, FINSEQ_1:55;
then A6: n = 1 by A5, TARSKI:def 1;
A7: (((1 - r) * p) + (r * q)) `1 = (((1 - r) * p) `1 ) + ((r * q) `1 ) by TOPREAL3:7
.= ((1 - r) * (p `1 )) + ((r * q) `1 ) by TOPREAL3:9
.= ((1 - r) * (p `1 )) + (r * (q `1 )) by TOPREAL3:9 ;
A8: ((1 - r) * (W-bound (L~ f))) + (r * (W-bound (L~ f))) = 1 * (W-bound (L~ f)) ;
A9: r * (W-bound (L~ f)) <= r * (q `1 ) by A1, A4, XREAL_1:66;
A10: 1 - r >= 0 by A2, XREAL_1:50;
then (1 - r) * (W-bound (L~ f)) <= (1 - r) * (p `1 ) by A4, XREAL_1:66;
then W-bound (L~ f) <= ((1 - r) * (p `1 )) + (r * (q `1 )) by A8, A9, XREAL_1:9;
hence W-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `1 by A6, A7, FINSEQ_4:25; :: thesis: ( (<*(((1 - r) * p) + (r * q))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `2 & (<*(((1 - r) * p) + (r * q))*> /. n) `2 <= N-bound (L~ f) )
A11: ((1 - r) * (E-bound (L~ f))) + (r * (E-bound (L~ f))) = 1 * (E-bound (L~ f)) ;
A12: r * (q `1 ) <= r * (E-bound (L~ f)) by A1, A4, XREAL_1:66;
(1 - r) * (p `1 ) <= (1 - r) * (E-bound (L~ f)) by A4, A10, XREAL_1:66;
then ((1 - r) * (p `1 )) + (r * (q `1 )) <= E-bound (L~ f) by A11, A12, XREAL_1:9;
hence (<*(((1 - r) * p) + (r * q))*> /. n) `1 <= E-bound (L~ f) by A6, A7, FINSEQ_4:25; :: thesis: ( S-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `2 & (<*(((1 - r) * p) + (r * q))*> /. n) `2 <= N-bound (L~ f) )
A13: (((1 - r) * p) + (r * q)) `2 = (((1 - r) * p) `2 ) + ((r * q) `2 ) by TOPREAL3:7
.= ((1 - r) * (p `2 )) + ((r * q) `2 ) by TOPREAL3:9
.= ((1 - r) * (p `2 )) + (r * (q `2 )) by TOPREAL3:9 ;
A14: ((1 - r) * (S-bound (L~ f))) + (r * (S-bound (L~ f))) = 1 * (S-bound (L~ f)) ;
A15: r * (S-bound (L~ f)) <= r * (q `2 ) by A1, A4, XREAL_1:66;
(1 - r) * (S-bound (L~ f)) <= (1 - r) * (p `2 ) by A4, A10, XREAL_1:66;
then S-bound (L~ f) <= ((1 - r) * (p `2 )) + (r * (q `2 )) by A14, A15, XREAL_1:9;
hence S-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `2 by A6, A13, FINSEQ_4:25; :: thesis: (<*(((1 - r) * p) + (r * q))*> /. n) `2 <= N-bound (L~ f)
A16: ((1 - r) * (N-bound (L~ f))) + (r * (N-bound (L~ f))) = 1 * (N-bound (L~ f)) ;
A17: r * (q `2 ) <= r * (N-bound (L~ f)) by A1, A4, XREAL_1:66;
(1 - r) * (p `2 ) <= (1 - r) * (N-bound (L~ f)) by A4, A10, XREAL_1:66;
then ((1 - r) * (p `2 )) + (r * (q `2 )) <= N-bound (L~ f) by A16, A17, XREAL_1:9;
hence (<*(((1 - r) * p) + (r * q))*> /. n) `2 <= N-bound (L~ f) by A6, A13, FINSEQ_4:25; :: thesis: verum