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: p .. f <= len f by A2, FINSEQ_4:31;
A5: len (f -: p) = p .. f by A2, FINSEQ_5:45;
then n in Seg (p .. f) by A3, FINSEQ_1:def 3;
then A6: (f -: p) /. n = f /. n by A2, FINSEQ_5:46;
n in Seg (len (f -: p)) by A3, FINSEQ_1:def 3;
then ( 1 <= n & n <= p .. f ) by A5, FINSEQ_1:3;
then ( 1 <= n & n <= len f ) by A4, XXREAL_0:2;
then n in dom f by FINSEQ_3:27;
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, A6, SPRECT_2:def 1; :: thesis: verum