let i be Nat; :: thesis: for f, g being FinSequence of (TOP-REAL 2) st g is_in_the_area_of f & i in dom g holds
<*(g /. i)*> is_in_the_area_of f
let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( g is_in_the_area_of f & i in dom g implies <*(g /. i)*> is_in_the_area_of f )
assume that
A1: g is_in_the_area_of f and
A2: i in dom g ; :: thesis: <*(g /. i)*> is_in_the_area_of f
let n be Nat; :: according to SPRECT_2:def 1 :: thesis: ( not n in dom <*(g /. i)*> or ( W-bound (L~ f) <= (<*(g /. i)*> /. n) `1 & (<*(g /. i)*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(g /. i)*> /. n) `2 & (<*(g /. i)*> /. n) `2 <= N-bound (L~ f) ) )
A3: dom <*(g /. i)*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
assume n in dom <*(g /. i)*> ; :: thesis: ( W-bound (L~ f) <= (<*(g /. i)*> /. n) `1 & (<*(g /. i)*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(g /. i)*> /. n) `2 & (<*(g /. i)*> /. n) `2 <= N-bound (L~ f) )
then n = 1 by A3, TARSKI:def 1;
then <*(g /. i)*> /. n = g /. i by FINSEQ_4:16;
hence ( W-bound (L~ f) <= (<*(g /. i)*> /. n) `1 & (<*(g /. i)*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(g /. i)*> /. n) `2 & (<*(g /. i)*> /. n) `2 <= N-bound (L~ f) ) by A1, A2; :: thesis: verum