let f be non 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:67;
A2: N-bound (L~ (SpStSeq (L~ f))) = N-bound (L~ f) by SPRECT_1:68;
A3: E-bound (L~ (SpStSeq (L~ f))) = E-bound (L~ f) by SPRECT_1:69;
A4: W-bound (L~ (SpStSeq (L~ f))) = W-bound (L~ f) by SPRECT_1:66;
thus ( g is_in_the_area_of f implies g is_in_the_area_of SpStSeq (L~ f) ) :: thesis: ( g is_in_the_area_of SpStSeq (L~ f) implies g is_in_the_area_of f )

proof

assume A5: g is_in_the_area_of f ; :: thesis: g is_in_the_area_of SpStSeq (L~ f)
let n be Element of NAT ; :: according to SPRECT_2:def 1 :: thesis: ( not n in dom g or ( W-bound (L~ (SpStSeq (L~ f))) <= (g /. n) `1 & (g /. n) `1 <= E-bound (L~ (SpStSeq (L~ f))) & S-bound (L~ (SpStSeq (L~ f))) <= (g /. n) `2 & (g /. n) `2 <= N-bound (L~ (SpStSeq (L~ f))) ) )
thus ( not n in dom g or ( W-bound (L~ (SpStSeq (L~ f))) <= (g /. n) `1 & (g /. n) `1 <= E-bound (L~ (SpStSeq (L~ f))) & S-bound (L~ (SpStSeq (L~ f))) <= (g /. n) `2 & (g /. n) `2 <= N-bound (L~ (SpStSeq (L~ f))) ) ) by A4, A1, A2, A3, A5, SPRECT_2:def 1; :: thesis: verum

end;

assume A6: g is_in_the_area_of SpStSeq (L~ f) ; :: thesis: g is_in_the_area_of f
let n be Element of 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, A6, SPRECT_2:def 1; :: thesis: verum