let i be Element of 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 Element of 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:4, FINSEQ_1:55;
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:25;
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, SPRECT_2:def 1; :: thesis: verum