let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds
for i, j being Nat st 1 <= i & i <= len G & 1 <= j & j <= width G & G * (i,j) in L~ f holds
G * (i,j) in rng f
let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G implies for i, j being Nat st 1 <= i & i <= len G & 1 <= j & j <= width G & G * (i,j) in L~ f holds
G * (i,j) in rng f )
assume A1: f is_sequence_on G ; :: thesis: for i, j being Nat st 1 <= i & i <= len G & 1 <= j & j <= width G & G * (i,j) in L~ f holds
G * (i,j) in rng f
let i, j be Nat; :: thesis: ( 1 <= i & i <= len G & 1 <= j & j <= width G & G * (i,j) in L~ f implies G * (i,j) in rng f )
assume that
A2: 1 <= i and
A3: i <= len G and
A4: 1 <= j and
A5: j <= width G ; :: thesis: ( not G * (i,j) in L~ f or G * (i,j) in rng f )
assume G * (i,j) in L~ f ; :: thesis: G * (i,j) in rng f
then consider k being Nat such that
A6: 1 <= k and
A7: k + 1 <= len f and
A8: G * (i,j) in LSeg ((f /. k),(f /. (k + 1))) by SPPOL_2:14;
consider i1, j1, i2, j2 being Nat such that
A9: [i1,j1] in Indices G and
A10: f /. k = G * (i1,j1) and
A11: [i2,j2] in Indices G and
A12: f /. (k + 1) = G * (i2,j2) and
A13: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A6, A7, JORDAN8:3;
A14: 1 <= i1 by A9, MATRIX_0:32;
A15: 1 <= j2 by A11, MATRIX_0:32;
A16: i2 <= len G by A11, MATRIX_0:32;
k + 1 >= 1 by NAT_1:11;
then A17: k + 1 in dom f by A7, FINSEQ_3:25;
A18: 1 <= j1 by A9, MATRIX_0:32;
k < len f by A7, NAT_1:13;
then A19: k in dom f by A6, FINSEQ_3:25;
A20: i1 <= len G by A9, MATRIX_0:32;
A21: j2 <= width G by A11, MATRIX_0:32;
A22: 1 <= i2 by A11, MATRIX_0:32;
A23: j1 <= width G by A9, MATRIX_0:32;

per cases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A13;

suppose A24: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: G * (i,j) in rng f

j1 <= j1 + 1 by NAT_1:11;
then A25: (G * (i1,j1)) `2 <= (G * (i1,(j1 + 1))) `2 by A14, A20, A18, A21, A24, JORDAN1A:19;
then (G * (i1,j1)) `2 <= (G * (i,j)) `2 by A8, A10, A12, A24, TOPREAL1:4;
then A26: j1 <= j by A2, A3, A4, A14, A20, A23, Th2;
A27: (G * (i1,j1)) `1 <= (G * (i1,(j1 + 1))) `1 by A14, A20, A18, A23, A15, A21, A24, JORDAN1A:18;
then (G * (i1,j1)) `1 <= (G * (i,j)) `1 by A8, A10, A12, A24, TOPREAL1:3;
then A28: i1 <= i by A2, A4, A5, A20, A18, A23, Th1;
(G * (i,j)) `2 <= (G * (i1,(j1 + 1))) `2 by A8, A10, A12, A24, A25, TOPREAL1:4;
then j <= j1 + 1 by A2, A3, A5, A14, A20, A15, A24, Th2;
then A29: ( j = j1 or j = j1 + 1 ) by A26, NAT_1:9;
(G * (i,j)) `1 <= (G * (i1,(j1 + 1))) `1 by A8, A10, A12, A24, A27, TOPREAL1:3;
then i <= i1 by A3, A4, A5, A14, A15, A21, A24, Th1;
then i = i1 by A28, XXREAL_0:1;
hence G * (i,j) in rng f by A10, A12, A19, A17, A24, A29, PARTFUN2:2; :: thesis: verum

end;

suppose A30: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: G * (i,j) in rng f

i1 <= i1 + 1 by NAT_1:11;
then A31: (G * (i1,j1)) `1 <= (G * ((i1 + 1),j1)) `1 by A14, A18, A23, A16, A30, JORDAN1A:18;
then (G * (i1,j1)) `1 <= (G * (i,j)) `1 by A8, A10, A12, A30, TOPREAL1:3;
then A32: i1 <= i by A2, A4, A5, A20, A18, A23, Th1;
A33: (G * (i1,j1)) `2 <= (G * ((i1 + 1),j1)) `2 by A14, A20, A18, A23, A22, A16, A30, JORDAN1A:19;
then (G * (i1,j1)) `2 <= (G * (i,j)) `2 by A8, A10, A12, A30, TOPREAL1:4;
then A34: j1 <= j by A2, A3, A4, A14, A20, A23, Th2;
(G * (i,j)) `1 <= (G * ((i1 + 1),j1)) `1 by A8, A10, A12, A30, A31, TOPREAL1:3;
then i <= i1 + 1 by A3, A4, A5, A18, A23, A22, A30, Th1;
then A35: ( i = i1 or i = i1 + 1 ) by A32, NAT_1:9;
(G * (i,j)) `2 <= (G * ((i1 + 1),j1)) `2 by A8, A10, A12, A30, A33, TOPREAL1:4;
then j <= j1 by A2, A3, A5, A18, A22, A16, A30, Th2;
then j = j1 by A34, XXREAL_0:1;
hence G * (i,j) in rng f by A10, A12, A19, A17, A30, A35, PARTFUN2:2; :: thesis: verum

end;

suppose A36: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: G * (i,j) in rng f

i2 <= i2 + 1 by NAT_1:11;
then A37: (G * (i2,j1)) `1 <= (G * ((i2 + 1),j1)) `1 by A20, A18, A23, A22, A36, JORDAN1A:18;
then (G * (i2,j1)) `1 <= (G * (i,j)) `1 by A8, A10, A12, A36, TOPREAL1:3;
then A38: i2 <= i by A2, A4, A5, A18, A23, A16, Th1;
A39: (G * (i2,j1)) `2 <= (G * ((i2 + 1),j1)) `2 by A14, A20, A18, A23, A22, A16, A36, JORDAN1A:19;
then (G * (i2,j1)) `2 <= (G * (i,j)) `2 by A8, A10, A12, A36, TOPREAL1:4;
then A40: j1 <= j by A2, A3, A4, A23, A22, A16, Th2;
(G * (i,j)) `1 <= (G * ((i2 + 1),j1)) `1 by A8, A10, A12, A36, A37, TOPREAL1:3;
then i <= i2 + 1 by A3, A4, A5, A14, A18, A23, A36, Th1;
then A41: ( i = i2 or i = i2 + 1 ) by A38, NAT_1:9;
(G * (i,j)) `2 <= (G * ((i2 + 1),j1)) `2 by A8, A10, A12, A36, A39, TOPREAL1:4;
then j <= j1 by A2, A3, A5, A14, A20, A18, A36, Th2;
then j = j1 by A40, XXREAL_0:1;
hence G * (i,j) in rng f by A10, A12, A19, A17, A36, A41, PARTFUN2:2; :: thesis: verum

end;

suppose A42: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: G * (i,j) in rng f

j2 <= j2 + 1 by NAT_1:11;
then A43: (G * (i1,j2)) `2 <= (G * (i1,(j2 + 1))) `2 by A14, A20, A23, A15, A42, JORDAN1A:19;
then (G * (i1,j2)) `2 <= (G * (i,j)) `2 by A8, A10, A12, A42, TOPREAL1:4;
then A44: j2 <= j by A2, A3, A4, A14, A20, A21, Th2;
A45: (G * (i1,j2)) `1 <= (G * (i1,(j2 + 1))) `1 by A14, A20, A18, A23, A15, A21, A42, JORDAN1A:18;
then (G * (i1,j2)) `1 <= (G * (i,j)) `1 by A8, A10, A12, A42, TOPREAL1:3;
then A46: i1 <= i by A2, A4, A5, A20, A15, A21, Th1;
(G * (i,j)) `2 <= (G * (i1,(j2 + 1))) `2 by A8, A10, A12, A42, A43, TOPREAL1:4;
then j <= j2 + 1 by A2, A3, A5, A14, A20, A18, A42, Th2;
then A47: ( j = j2 or j = j2 + 1 ) by A44, NAT_1:9;
(G * (i,j)) `1 <= (G * (i1,(j2 + 1))) `1 by A8, A10, A12, A42, A45, TOPREAL1:3;
then i <= i1 by A3, A4, A5, A14, A18, A23, A42, Th1;
then i = i1 by A46, XXREAL_0:1;
hence G * (i,j) in rng f by A10, A12, A19, A17, A42, A47, PARTFUN2:2; :: thesis: verum

end;

end;