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 Element of 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) ) )
assume A3: 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) )
A4: len (f :- p) = ((len f) - (p .. f)) + 1 by A2, FINSEQ_5:53;
n in Seg (len (f :- p)) by A3, FINSEQ_1:def 3;
then A5: ( 0 + 1 <= n & n <= ((len f) - (p .. f)) + 1 ) by A4, FINSEQ_1:3;
1 <= p .. f by A2, FINSEQ_4:31;
then A7: 0 + 1 <= (n -' 1) + (p .. f) by XREAL_1:9;
A8: n - 1 >= 0 by A5, XREAL_1:21;
n - 1 <= (len f) - (p .. f) by A5, XREAL_1:22;
then (n - 1) + (p .. f) <= len f by XREAL_1:21;
then (n -' 1) + (p .. f) <= len f by A8, XREAL_0:def 2;
then A9: (n -' 1) + (p .. f) in dom f by A7, FINSEQ_3:27;
(n -' 1) + 1 = n by A5, XREAL_1:237;
then (f :- p) /. n = f /. ((n -' 1) + (p .. f)) by A2, A3, FINSEQ_5:55;
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, A9, SPRECT_2:def 1; :: thesis: verum