let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( g is_in_the_area_of f implies for i, j being 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 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 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 Nat; :: thesis: ( i in dom g & j in dom g implies mid (g,i,j) is_in_the_area_of f )
assume A2: ( i in dom g & 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 A3: i <= j ; :: thesis: mid (g,i,j) is_in_the_area_of f

let n be 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 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 ( (n + i) -' 1 in dom g & (mid (g,i,j)) /. n = g /. ((n + i) -' 1) ) by A2, A3, Th1, Th3;
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; :: thesis: verum

end;

suppose A4: i > j ; :: thesis: mid (g,i,j) is_in_the_area_of f

let n be 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 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 ( (i -' n) + 1 in dom g & (mid (g,i,j)) /. n = g /. ((i -' n) + 1) ) by A2, A4, Th2, Th4;
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; :: thesis: verum

end;

end;