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 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 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 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, Th5, 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; :: thesis: verum

end;

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 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, Th6, 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; :: thesis: verum

end;

end;