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
then A3: p .. f <= len f by FINSEQ_4:21;
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) ) )
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) )
A5: len (f -: p) = p .. f by A2, FINSEQ_5:42;
then n in Seg (p .. f) by A4, FINSEQ_1:def 3;
then A6: (f -: p) /. n = f /. n by A2, FINSEQ_5:43;
A7: n in Seg (len (f -: p)) by A4, FINSEQ_1:def 3;
then n <= p .. f by A5, FINSEQ_1:1;
then A8: n <= len f by A3, XXREAL_0:2;
1 <= n by A7, FINSEQ_1:1;
then n in dom f by A8, 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, A6; :: thesis: verum