let m, k be Element of NAT ; for G being Go-board st width G = m + 1 & m > 0 & k in Seg m holds
( Col (DelCol G,(width G)),k = Col G,k & k in Seg (width (DelCol G,(width G))) )
let G be Go-board; ( width G = m + 1 & m > 0 & k in Seg m implies ( Col (DelCol G,(width G)),k = Col G,k & k in Seg (width (DelCol G,(width G))) ) )
assume that
A1:
width G = m + 1
and
A2:
m > 0
and
A3:
k in Seg m
; ( Col (DelCol G,(width G)),k = Col G,k & k in Seg (width (DelCol G,(width G))) )
k <= m
by A3, FINSEQ_1:3;
then A4:
k < width G
by A1, NAT_1:13;
1 <= width G
by A1, A2, Th3;
then A5:
width G in Seg (width G)
by FINSEQ_1:3;
1 <= k
by A3, FINSEQ_1:3;
hence
( Col (DelCol G,(width G)),k = Col G,k & k in Seg (width (DelCol G,(width G))) )
by A1, A2, A5, A4, Th29; verum