let f be FinSequence of (TOP-REAL 2); :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 A1:
( 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 )
; :: thesis: f /. n in rng (Line (DelCol G,i),m)
then consider j being Nat such that
A2:
( j in dom (Line G,m) & f /. n = (Line G,m) . j )
by FINSEQ_2:11;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
A3:
dom (Line G,m) = Seg (len (Line G,m))
by FINSEQ_1:def 3;
len (Line G,m) = width G
by MATRIX_1:def 8;
then A4:
( f /. n = G * m,j & 1 <= j & j <= width G & 1 <= i & i <= width G & len (Line (DelCol G,i),m) = width (DelCol G,i) & dom (Line (DelCol G,i),m) = Seg (len (Line (DelCol G,i),m)) )
by A1, A2, A3, FINSEQ_1:def 3, FINSEQ_3:27, MATRIX_1:def 8;
then A5:
j <> i
by A1, Th24;
consider M being Element of NAT such that
A6:
( width G = M + 1 & M > 0 )
by A1, Th3;
A7:
width (DelCol G,i) = M
by A1, A6, Th26;
per cases
( j < i or i < j )
by A5, XXREAL_0:1;
suppose A8:
j < i
;
:: thesis: f /. n in rng (Line (DelCol G,i),m)then A9:
f /. n = (DelCol G,i) * m,
j
by A1, A4, A6, Th31;
j < width G
by A4, A8, XXREAL_0:2;
then
j <= M
by A6, NAT_1:13;
then
j in Seg (width (DelCol G,i))
by A4, A7, FINSEQ_1:3;
then
(
(Line (DelCol G,i),m) . j = f /. n &
(Line (DelCol G,i),m) . j in rng (Line (DelCol G,i),m) )
by A4, A9, FUNCT_1:def 5, MATRIX_1:def 8;
hence
f /. n in rng (Line (DelCol G,i),m)
;
:: thesis: verum end; suppose
i < j
;
:: thesis: f /. n in rng (Line (DelCol G,i),m)then A10:
( 1
< j &
i + 1
<= j )
by A4, NAT_1:13, XXREAL_0:2;
reconsider l =
j - 1 as
Element of
NAT by A4, INT_1:18;
A11:
(
i <= l &
l <= M &
l + 1
= j )
by A4, A6, A10, XREAL_1:21, XREAL_1:22;
then A12:
(
f /. n = (DelCol G,i) * m,
l & 1
<= l )
by A1, A4, A6, Th32, XXREAL_0:2;
then
l in Seg (width (DelCol G,i))
by A7, A11, FINSEQ_1:3;
then
(
(Line (DelCol G,i),m) . l = f /. n &
(Line (DelCol G,i),m) . l in rng (Line (DelCol G,i),m) )
by A4, A12, FUNCT_1:def 5, MATRIX_1:def 8;
hence
f /. n in rng (Line (DelCol G,i),m)
;
:: thesis: verum end;