let i, j be Nat; :: thesis: for f being constant standard special_circular_sequence st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds
<*((GoB f) * (i,j))*> is_in_the_area_of f
let f be constant standard special_circular_sequence; :: thesis: ( 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) implies <*((GoB f) * (i,j))*> is_in_the_area_of f )
assume that
A1: 1 <= i and
A2: i <= len (GoB f) and
A3: 1 <= j and
A4: j <= width (GoB f) ; :: thesis: <*((GoB f) * (i,j))*> is_in_the_area_of f
set G = GoB f;
A5: 1 <= width (GoB f) by A3, A4, XXREAL_0:2;
A6: 1 <= len (GoB f) by A1, A2, XXREAL_0:2;
A7: N-bound (L~ f) = ((GoB f) * (1,(width (GoB f)))) `2 by JORDAN5D:40
.= ((GoB f) * (i,(width (GoB f)))) `2 by A1, A2, A5, GOBOARD5:1 ;
A8: ( j = 1 or j > 1 ) by A3, XXREAL_0:1;
A9: S-bound (L~ f) = ((GoB f) * (1,1)) `2 by JORDAN5D:38
.= ((GoB f) * (i,1)) `2 by A1, A2, A5, GOBOARD5:1 ;
A10: ( i = 1 or i > 1 ) by A1, XXREAL_0:1;
A11: E-bound (L~ f) = ((GoB f) * ((len (GoB f)),1)) `1 by JORDAN5D:39
.= ((GoB f) * ((len (GoB f)),j)) `1 by A3, A4, A6, GOBOARD5:2 ;
A12: ( j = width (GoB f) or j < width (GoB f) ) by A4, XXREAL_0:1;
A13: ( i = len (GoB f) or i < len (GoB f) ) by A2, XXREAL_0:1;
let n be Nat; :: according to SPRECT_2:def 1 :: thesis: ( not n in dom <*((GoB f) * (i,j))*> or ( W-bound (L~ f) <= (<*((GoB f) * (i,j))*> /. n) `1 & (<*((GoB f) * (i,j))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*((GoB f) * (i,j))*> /. n) `2 & (<*((GoB f) * (i,j))*> /. n) `2 <= N-bound (L~ f) ) )
set p = (GoB f) * (i,j);
assume n in dom <*((GoB f) * (i,j))*> ; :: thesis: ( W-bound (L~ f) <= (<*((GoB f) * (i,j))*> /. n) `1 & (<*((GoB f) * (i,j))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*((GoB f) * (i,j))*> /. n) `2 & (<*((GoB f) * (i,j))*> /. n) `2 <= N-bound (L~ f) )
then n in {1} by FINSEQ_1:2, FINSEQ_1:38;
then n = 1 by TARSKI:def 1;
then A14: <*((GoB f) * (i,j))*> /. n = (GoB f) * (i,j) by FINSEQ_4:16;
W-bound (L~ f) = ((GoB f) * (1,1)) `1 by JORDAN5D:37
.= ((GoB f) * (1,j)) `1 by A3, A4, A6, GOBOARD5:2 ;
hence ( W-bound (L~ f) <= (<*((GoB f) * (i,j))*> /. n) `1 & (<*((GoB f) * (i,j))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*((GoB f) * (i,j))*> /. n) `2 & (<*((GoB f) * (i,j))*> /. n) `2 <= N-bound (L~ f) ) by A14, A10, A9, A8, A11, A13, A7, A12, GOBOARD5:3, GOBOARD5:4; :: thesis: verum