let i, j be Element of NAT ; :: thesis: for f being non 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 non 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:42
.= ((GoB f) * i,(width (GoB f))) `2 by A1, A2, A5, GOBOARD5:2 ;
A8: ( j = 1 or j > 1 ) by A3, XXREAL_0:1;
A9: S-bound (L~ f) = ((GoB f) * 1,1) `2 by JORDAN5D:40
.= ((GoB f) * i,1) `2 by A1, A2, A5, GOBOARD5:2 ;
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:41
.= ((GoB f) * (len (GoB f)),j) `1 by A3, A4, A6, GOBOARD5:3 ;
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 Element of 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:4, FINSEQ_1:55;
then n = 1 by TARSKI:def 1;
then A14: <*((GoB f) * i,j)*> /. n = (GoB f) * i,j by FINSEQ_4:25;
W-bound (L~ f) = ((GoB f) * 1,1) `1 by JORDAN5D:39
.= ((GoB f) * 1,j) `1 by A3, A4, A6, GOBOARD5:3 ;
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:4, GOBOARD5:5; :: thesis: verum