let f be constant standard special_circular_sequence; :: thesis: for g being FinSequence of (TOP-REAL 2) holds
( g is_in_the_area_of f iff g is_in_the_area_of SpStSeq (L~ f) )
let g be FinSequence of (TOP-REAL 2); :: thesis: ( g is_in_the_area_of f iff g is_in_the_area_of SpStSeq (L~ f) )
A1: S-bound (L~ (SpStSeq (L~ f))) = S-bound (L~ f) by SPRECT_1:59;
A2: N-bound (L~ (SpStSeq (L~ f))) = N-bound (L~ f) by SPRECT_1:60;
A3: E-bound (L~ (SpStSeq (L~ f))) = E-bound (L~ f) by SPRECT_1:61;
A4: W-bound (L~ (SpStSeq (L~ f))) = W-bound (L~ f) by SPRECT_1:58;
thus ( g is_in_the_area_of f implies g is_in_the_area_of SpStSeq (L~ f) ) by A4, A1, A2, A3; :: thesis: ( g is_in_the_area_of SpStSeq (L~ f) implies g is_in_the_area_of f )
assume A5: g is_in_the_area_of SpStSeq (L~ f) ; :: thesis: g is_in_the_area_of f
let n be Nat; :: according to SPRECT_2:def 1 :: thesis: ( not n in dom g or ( W-bound (L~ f) <= (g /. n) `1 & (g /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (g /. n) `2 & (g /. n) `2 <= N-bound (L~ f) ) )
thus ( not n in dom g or ( W-bound (L~ f) <= (g /. n) `1 & (g /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (g /. n) `2 & (g /. n) `2 <= N-bound (L~ f) ) ) by A4, A1, A2, A3, A5; :: thesis: verum