let f be FinSequence of (TOP-REAL 2); for i, n, m being Element of NAT
for G being Go-board st rng f misses rng (Col G,i) & f /. n in rng (Line G,m) & n in dom f & i in Seg (width G) & m in dom G & width G > 1 holds
f /. n in rng (Line (DelCol G,i),m)
let i, n, m be Element of NAT ; for G being Go-board st rng f misses rng (Col G,i) & f /. n in rng (Line G,m) & n in dom f & i in Seg (width G) & m in dom G & width G > 1 holds
f /. n in rng (Line (DelCol G,i),m)
let G be Go-board; ( rng f misses rng (Col G,i) & f /. n in rng (Line G,m) & n in dom f & i in Seg (width G) & m in dom G & width G > 1 implies f /. n in rng (Line (DelCol G,i),m) )
set D = DelCol G,i;
assume that
A1:
rng f misses rng (Col G,i)
and
A2:
f /. n in rng (Line G,m)
and
A3:
n in dom f
and
A4:
i in Seg (width G)
and
A5:
m in dom G
and
A6:
width G > 1
; f /. n in rng (Line (DelCol G,i),m)
A7:
( len (Line (DelCol G,i),m) = width (DelCol G,i) & dom (Line (DelCol G,i),m) = Seg (len (Line (DelCol G,i),m)) )
by FINSEQ_1:def 3, MATRIX_1:def 8;
consider j being Nat such that
A8:
j in dom (Line G,m)
and
A9:
f /. n = (Line G,m) . j
by A2, FINSEQ_2:11;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
A10:
len (Line G,m) = width G
by MATRIX_1:def 8;
then A11:
j <= width G
by A8, FINSEQ_3:27;
A12:
dom (Line G,m) = Seg (len (Line G,m))
by FINSEQ_1:def 3;
then A13:
1 <= i
by A4, A10, FINSEQ_3:27;
A14:
f /. n = G * m,j
by A8, A9, A12, A10, MATRIX_1:def 8;
A15:
i <= width G
by A4, A12, A10, FINSEQ_3:27;
A16:
1 <= j
by A8, FINSEQ_3:27;
consider M being Element of NAT such that
A17:
width G = M + 1
and
A18:
M > 0
by A6, Th3;
A19:
width (DelCol G,i) = M
by A4, A17, A18, Th26;
per cases
( j < i or i < j )
by A1, A3, A5, A14, Th24, XXREAL_0:1;
suppose A20:
j < i
;
f /. n in rng (Line (DelCol G,i),m)then
j < width G
by A15, XXREAL_0:2;
then
j <= M
by A17, NAT_1:13;
then A21:
j in Seg (width (DelCol G,i))
by A16, A19, FINSEQ_1:3;
f /. n = (DelCol G,i) * m,
j
by A4, A5, A14, A16, A17, A18, A20, Th31;
then
(Line (DelCol G,i),m) . j = f /. n
by A21, MATRIX_1:def 8;
hence
f /. n in rng (Line (DelCol G,i),m)
by A7, A21, FUNCT_1:def 5;
verum end; suppose A22:
i < j
;
f /. n in rng (Line (DelCol G,i),m)reconsider l =
j - 1 as
Element of
NAT by A16, INT_1:18;
A23:
l <= M
by A11, A17, XREAL_1:22;
i + 1
<= j
by A22, NAT_1:13;
then A24:
i <= l
by XREAL_1:21;
then
1
<= l
by A13, XXREAL_0:2;
then A25:
l in Seg (width (DelCol G,i))
by A19, A23, FINSEQ_1:3;
l + 1
= j
;
then
f /. n = (DelCol G,i) * m,
l
by A4, A5, A14, A13, A17, A24, A23, Th32;
then
(Line (DelCol G,i),m) . l = f /. n
by A25, MATRIX_1:def 8;
hence
f /. n in rng (Line (DelCol G,i),m)
by A7, A25, FUNCT_1:def 5;
verum end;