let i, j be Nat; :: thesis: for f being V22() 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 V22() 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

<*((GoB f) * (i,j))*> is_in_the_area_of f

let f be V22() 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