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, SEQM_3:83;
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;