let i, m, k be Element of NAT ; for G being Go-board st i in Seg (width G) & width G = m + 1 & m > 0 & i <= k & k <= m holds
( Col (DelCol G,i),k = Col G,(k + 1) & k in Seg (width (DelCol G,i)) & k + 1 in Seg (width G) )
let G be Go-board; ( i in Seg (width G) & width G = m + 1 & m > 0 & i <= k & k <= m implies ( Col (DelCol G,i),k = Col G,(k + 1) & k in Seg (width (DelCol G,i)) & k + 1 in Seg (width G) ) )
set N = DelCol G,i;
assume that
A1:
i in Seg (width G)
and
A2:
width G = m + 1
and
A3:
m > 0
and
A4:
i <= k
and
A5:
k <= m
; ( Col (DelCol G,i),k = Col G,(k + 1) & k in Seg (width (DelCol G,i)) & k + 1 in Seg (width G) )
A6:
len (Col (DelCol G,i),k) = len (DelCol G,i)
by MATRIX_1:def 9;
A7:
1 < width G
by A2, A3, Th3;
then A8:
len (DelCol G,i) = len G
by A1, Def10;
A9:
( 1 <= k + 1 & k + 1 <= m + 1 )
by A5, NAT_1:11, XREAL_1:8;
then A10:
k + 1 in Seg (width G)
by A2, FINSEQ_1:3;
1 <= i
by A1, FINSEQ_1:3;
then A11:
1 <= k
by A4, XXREAL_0:2;
A12:
len (Col G,(k + 1)) = len G
by MATRIX_1:def 9;
A13:
width (DelCol G,i) = m
by A1, A2, A3, Th26;
then A14:
k in Seg (width (DelCol G,i))
by A5, A11, FINSEQ_1:3;
now let j be
Nat;
( 1 <= j & j <= len (Col (DelCol G,i),k) implies (Col (DelCol G,i),k) . j = (Col G,(k + 1)) . j )A15:
(
dom (DelCol G,i) = Seg (len (DelCol G,i)) &
dom G = Seg (len G) )
by FINSEQ_1:def 3;
A16:
(
len (Line G,j) = m + 1 &
dom (Line G,j) = Seg (len (Line G,j)) )
by A2, FINSEQ_1:def 3, MATRIX_1:def 8;
assume
( 1
<= j &
j <= len (Col (DelCol G,i),k) )
;
(Col (DelCol G,i),k) . j = (Col G,(k + 1)) . jthen A17:
j in dom (DelCol G,i)
by A6, FINSEQ_3:27;
hence (Col (DelCol G,i),k) . j =
(DelCol G,i) * j,
k
by MATRIX_1:def 9
.=
(Del (Line G,j),i) . k
by A1, A14, A7, A8, A17, A15, Th28
.=
(Line G,j) . (k + 1)
by A1, A2, A4, A5, A16, FINSEQ_3:120
.=
(Col G,(k + 1)) . j
by A10, A8, A17, A15, Th17
;
verum end;
hence
( Col (DelCol G,i),k = Col G,(k + 1) & k in Seg (width (DelCol G,i)) & k + 1 in Seg (width G) )
by A2, A5, A13, A9, A11, A6, A12, A8, FINSEQ_1:3, FINSEQ_1:18; verum