let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( f is_in_the_area_of g implies for p being Element of (TOP-REAL 2) st p in rng f holds
f :- p is_in_the_area_of g )
assume A1: f is_in_the_area_of g ; :: thesis: for p being Element of (TOP-REAL 2) st p in rng f holds
f :- p is_in_the_area_of g
let p be Element of (TOP-REAL 2); :: thesis: ( p in rng f implies f :- p is_in_the_area_of g )
assume A2: p in rng f ; :: thesis: f :- p is_in_the_area_of g
let n be Nat; :: according to SPRECT_2:def 1 :: thesis: ( not n in dom (f :- p) or ( W-bound (L~ g) <= ((f :- p) /. n) `1 & ((f :- p) /. n) `1 <= E-bound (L~ g) & S-bound (L~ g) <= ((f :- p) /. n) `2 & ((f :- p) /. n) `2 <= N-bound (L~ g) ) )
1 <= p .. f by A2, FINSEQ_4:21;
then A3: 0 + 1 <= (n -' 1) + (p .. f) by XREAL_1:7;
assume A4: n in dom (f :- p) ; :: thesis: ( W-bound (L~ g) <= ((f :- p) /. n) `1 & ((f :- p) /. n) `1 <= E-bound (L~ g) & S-bound (L~ g) <= ((f :- p) /. n) `2 & ((f :- p) /. n) `2 <= N-bound (L~ g) )
then A5: n in Seg (len (f :- p)) by FINSEQ_1:def 3;
then A6: 0 + 1 <= n by FINSEQ_1:1;
then (n -' 1) + 1 = n by XREAL_1:235;
then A7: (f :- p) /. n = f /. ((n -' 1) + (p .. f)) by A2, A4, FINSEQ_5:52;
len (f :- p) = ((len f) - (p .. f)) + 1 by A2, FINSEQ_5:50;
then n <= ((len f) - (p .. f)) + 1 by A5, FINSEQ_1:1;
then n - 1 <= (len f) - (p .. f) by XREAL_1:20;
then A8: (n - 1) + (p .. f) <= len f by XREAL_1:19;
n - 1 >= 0 by A6, XREAL_1:19;
then (n -' 1) + (p .. f) <= len f by A8, XREAL_0:def 2;
then (n -' 1) + (p .. f) in dom f by A3, FINSEQ_3:25;
hence ( W-bound (L~ g) <= ((f :- p) /. n) `1 & ((f :- p) /. n) `1 <= E-bound (L~ g) & S-bound (L~ g) <= ((f :- p) /. n) `2 & ((f :- p) /. n) `2 <= N-bound (L~ g) ) by A1, A7; :: thesis: verum