let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( g is_in_the_area_of f implies for i, j being Element of NAT st i in dom g & j in dom g holds
mid g,i,j is_in_the_area_of f )
assume A1: for n being Element of NAT st n in dom g holds
( 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) ) ; :: according to SPRECT_2:def 1 :: thesis: for i, j being Element of NAT st i in dom g & j in dom g holds
mid g,i,j is_in_the_area_of f
let i, j be Element of NAT ; :: thesis: ( i in dom g & j in dom g implies mid g,i,j is_in_the_area_of f )
assume that
A2: i in dom g and
A3: j in dom g ; :: thesis: mid g,i,j is_in_the_area_of f
set h = mid g,i,j;

per cases ( i <= j or i > j ) ;

suppose A4: i <= j ; :: thesis: mid g,i,j is_in_the_area_of f

let n be Element of NAT ; :: according to SPRECT_2:def 1 :: thesis: ( n in dom (mid g,i,j) implies ( W-bound (L~ f) <= ((mid g,i,j) /. n) `1 & ((mid g,i,j) /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= ((mid g,i,j) /. n) `2 & ((mid g,i,j) /. n) `2 <= N-bound (L~ f) ) )
assume A5: n in dom (mid g,i,j) ; :: thesis: ( W-bound (L~ f) <= ((mid g,i,j) /. n) `1 & ((mid g,i,j) /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= ((mid g,i,j) /. n) `2 & ((mid g,i,j) /. n) `2 <= N-bound (L~ f) )
then A6: (n + i) -' 1 in dom g by A2, A3, A4, Th5;
(mid g,i,j) /. n = g /. ((n + i) -' 1) by A2, A3, A4, A5, Th7;
hence ( W-bound (L~ f) <= ((mid g,i,j) /. n) `1 & ((mid g,i,j) /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= ((mid g,i,j) /. n) `2 & ((mid g,i,j) /. n) `2 <= N-bound (L~ f) ) by A1, A6; :: thesis: verum

end;

suppose A7: i > j ; :: thesis: mid g,i,j is_in_the_area_of f

let n be Element of NAT ; :: according to SPRECT_2:def 1 :: thesis: ( n in dom (mid g,i,j) implies ( W-bound (L~ f) <= ((mid g,i,j) /. n) `1 & ((mid g,i,j) /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= ((mid g,i,j) /. n) `2 & ((mid g,i,j) /. n) `2 <= N-bound (L~ f) ) )
assume A8: n in dom (mid g,i,j) ; :: thesis: ( W-bound (L~ f) <= ((mid g,i,j) /. n) `1 & ((mid g,i,j) /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= ((mid g,i,j) /. n) `2 & ((mid g,i,j) /. n) `2 <= N-bound (L~ f) )
then A9: (i -' n) + 1 in dom g by A2, A3, A7, Th6;
(mid g,i,j) /. n = g /. ((i -' n) + 1) by A2, A3, A7, A8, Th8;
hence ( W-bound (L~ f) <= ((mid g,i,j) /. n) `1 & ((mid g,i,j) /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= ((mid g,i,j) /. n) `2 & ((mid g,i,j) /. n) `2 <= N-bound (L~ f) ) by A1, A9; :: thesis: verum

end;

end;