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
A4: dom <*p,q*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
then A5: 2 in dom <*p,q*> by TARSKI:def 2;
A6: <*p,q*> /. 2 = q by FINSEQ_4:17;
then W-bound (L~ f) <= q `1 by A3, A5;
then A7: r * (W-bound (L~ f)) <= r * (q `1) by A1, XREAL_1:64;
q `1 <= E-bound (L~ f) by A3, A5, A6;
then A8: r * (q `1) <= r * (E-bound (L~ f)) by A1, XREAL_1:64;
A9: <*p,q*> /. 1 = p by FINSEQ_4:17;
A10: 1 - r >= 0 by A2, XREAL_1:48;
A11: 1 in dom <*p,q*> by A4, TARSKI:def 2;
then W-bound (L~ f) <= p `1 by A3, A9;
then A12: (1 - r) * (W-bound (L~ f)) <= (1 - r) * (p `1) by A10, XREAL_1:64;
p `1 <= E-bound (L~ f) by A3, A11, A9;
then A13: (1 - r) * (p `1) <= (1 - r) * (E-bound (L~ f)) by A10, XREAL_1:64;
S-bound (L~ f) <= p `2 by A3, A11, A9;
then A14: (1 - r) * (S-bound (L~ f)) <= (1 - r) * (p `2) by A10, XREAL_1:64;
A15: (((1 - r) * p) + (r * q)) `1 = (((1 - r) * p) `1) + ((r * q) `1) by TOPREAL3:2
.= ((1 - r) * (p `1)) + ((r * q) `1) by TOPREAL3:4
.= ((1 - r) * (p `1)) + (r * (q `1)) by TOPREAL3:4 ;
p `2 <= N-bound (L~ f) by A3, A11, A9;
then A16: (1 - r) * (p `2) <= (1 - r) * (N-bound (L~ f)) by A10, XREAL_1:64;
let n be 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) ) )
A17: dom <*(((1 - r) * p) + (r * q))*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
assume 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) )
then A18: n = 1 by A17, TARSKI:def 1;
((1 - r) * (W-bound (L~ f))) + (r * (W-bound (L~ f))) = 1 * (W-bound (L~ f)) ;
then W-bound (L~ f) <= ((1 - r) * (p `1)) + (r * (q `1)) by A7, A12, XREAL_1:7;
hence W-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `1 by A18, A15, FINSEQ_4:16; :: 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) )
((1 - r) * (E-bound (L~ f))) + (r * (E-bound (L~ f))) = 1 * (E-bound (L~ f)) ;
then ((1 - r) * (p `1)) + (r * (q `1)) <= E-bound (L~ f) by A8, A13, XREAL_1:7;
hence (<*(((1 - r) * p) + (r * q))*> /. n) `1 <= E-bound (L~ f) by A18, A15, FINSEQ_4:16; :: thesis: ( S-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `2 & (<*(((1 - r) * p) + (r * q))*> /. n) `2 <= N-bound (L~ f) )
A19: (((1 - r) * p) + (r * q)) `2 = (((1 - r) * p) `2) + ((r * q) `2) by TOPREAL3:2
.= ((1 - r) * (p `2)) + ((r * q) `2) by TOPREAL3:4
.= ((1 - r) * (p `2)) + (r * (q `2)) by TOPREAL3:4 ;
q `2 <= N-bound (L~ f) by A3, A5, A6;
then A20: r * (q `2) <= r * (N-bound (L~ f)) by A1, XREAL_1:64;
S-bound (L~ f) <= q `2 by A3, A5, A6;
then A21: r * (S-bound (L~ f)) <= r * (q `2) by A1, XREAL_1:64;
((1 - r) * (S-bound (L~ f))) + (r * (S-bound (L~ f))) = 1 * (S-bound (L~ f)) ;
then S-bound (L~ f) <= ((1 - r) * (p `2)) + (r * (q `2)) by A21, A14, XREAL_1:7;
hence S-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `2 by A18, A19, FINSEQ_4:16; :: thesis: (<*(((1 - r) * p) + (r * q))*> /. n) `2 <= N-bound (L~ f)
((1 - r) * (N-bound (L~ f))) + (r * (N-bound (L~ f))) = 1 * (N-bound (L~ f)) ;
then ((1 - r) * (p `2)) + (r * (q `2)) <= N-bound (L~ f) by A20, A16, XREAL_1:7;
hence (<*(((1 - r) * p) + (r * q))*> /. n) `2 <= N-bound (L~ f) by A18, A19, FINSEQ_4:16; :: thesis: verum