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 Element of 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 Element of 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 Element of 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 Element of 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 A2: ( 1 <= i & i <= len G & 1 <= j & 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 Element of NAT such that
A3: 1 <= k and
A4: k + 1 <= len f and
A5: G * i,j in LSeg (f /. k),(f /. (k + 1)) by SPPOL_2:14;
consider i1, j1, i2, j2 being Element of NAT such that
A6: [i1,j1] in Indices G and
A7: f /. k = G * i1,j1 and
A8: [i2,j2] in Indices G and
A9: f /. (k + 1) = G * i2,j2 and
A10: ( ( 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, A3, A4, JORDAN8:6;
A11: ( 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G ) by A6, MATRIX_1:39;
A12: ( 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G ) by A8, MATRIX_1:39;
( k + 1 >= 1 & k < len f ) by A4, NAT_1:11, NAT_1:13;
then A13: ( k in dom f & k + 1 in dom f ) by A3, A4, FINSEQ_3:27;

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 A10;

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

j1 <= j1 + 1 by NAT_1:11;
then ( (G * i1,j1) `1 <= (G * i1,(j1 + 1)) `1 & (G * i1,j1) `2 <= (G * i1,(j1 + 1)) `2 ) by A11, A12, A14, JORDAN1A:39, JORDAN1A:40;
then ( (G * i1,j1) `1 <= (G * i,j) `1 & (G * i,j) `1 <= (G * i1,(j1 + 1)) `1 & (G * i1,j1) `2 <= (G * i,j) `2 & (G * i,j) `2 <= (G * i1,(j1 + 1)) `2 ) by A5, A7, A9, A14, TOPREAL1:9, TOPREAL1:10;
then ( i1 <= i & i <= i1 & j1 <= j & j <= j1 + 1 ) by A2, A11, A12, A14, Th1, Th2;
then ( i = i1 & ( j = j1 or j = j1 + 1 ) ) by NAT_1:9, XXREAL_0:1;
hence G * i,j in rng f by A7, A9, A13, A14, PARTFUN2:4; :: thesis: verum

end;

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

i1 <= i1 + 1 by NAT_1:11;
then ( (G * i1,j1) `1 <= (G * (i1 + 1),j1) `1 & (G * i1,j1) `2 <= (G * (i1 + 1),j1) `2 ) by A11, A12, A15, JORDAN1A:39, JORDAN1A:40;
then ( (G * i1,j1) `1 <= (G * i,j) `1 & (G * i,j) `1 <= (G * (i1 + 1),j1) `1 & (G * i1,j1) `2 <= (G * i,j) `2 & (G * i,j) `2 <= (G * (i1 + 1),j1) `2 ) by A5, A7, A9, A15, TOPREAL1:9, TOPREAL1:10;
then ( j1 <= j & j <= j1 & i1 <= i & i <= i1 + 1 ) by A2, A11, A12, A15, Th1, Th2;
then ( j = j1 & ( i = i1 or i = i1 + 1 ) ) by NAT_1:9, XXREAL_0:1;
hence G * i,j in rng f by A7, A9, A13, A15, PARTFUN2:4; :: thesis: verum

end;

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

i2 <= i2 + 1 by NAT_1:11;
then ( (G * i2,j1) `1 <= (G * (i2 + 1),j1) `1 & (G * i2,j1) `2 <= (G * (i2 + 1),j1) `2 ) by A11, A12, A16, JORDAN1A:39, JORDAN1A:40;
then ( (G * i2,j1) `1 <= (G * i,j) `1 & (G * i,j) `1 <= (G * (i2 + 1),j1) `1 & (G * i2,j1) `2 <= (G * i,j) `2 & (G * i,j) `2 <= (G * (i2 + 1),j1) `2 ) by A5, A7, A9, A16, TOPREAL1:9, TOPREAL1:10;
then ( j1 <= j & j <= j1 & i2 <= i & i <= i2 + 1 ) by A2, A11, A12, A16, Th1, Th2;
then ( j = j1 & ( i = i2 or i = i2 + 1 ) ) by NAT_1:9, XXREAL_0:1;
hence G * i,j in rng f by A7, A9, A13, A16, PARTFUN2:4; :: thesis: verum

end;

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

j2 <= j2 + 1 by NAT_1:11;
then ( (G * i1,j2) `1 <= (G * i1,(j2 + 1)) `1 & (G * i1,j2) `2 <= (G * i1,(j2 + 1)) `2 ) by A11, A12, A17, JORDAN1A:39, JORDAN1A:40;
then ( (G * i1,j2) `1 <= (G * i,j) `1 & (G * i,j) `1 <= (G * i1,(j2 + 1)) `1 & (G * i1,j2) `2 <= (G * i,j) `2 & (G * i,j) `2 <= (G * i1,(j2 + 1)) `2 ) by A5, A7, A9, A17, TOPREAL1:9, TOPREAL1:10;
then ( i1 <= i & i <= i1 & j2 <= j & j <= j2 + 1 ) by A2, A11, A12, A17, Th1, Th2;
then ( i = i1 & ( j = j2 or j = j2 + 1 ) ) by NAT_1:9, XXREAL_0:1;
hence G * i,j in rng f by A7, A9, A13, A17, PARTFUN2:4; :: thesis: verum

end;

end;