let m, i, j, k be Nat; for x being set
for G being Go-board st x = G * (m,k) & x = G * (i,j) & [m,k] in Indices G & [i,j] in Indices G holds
( m = i & k = j )
let x be set ; for G being Go-board st x = G * (m,k) & x = G * (i,j) & [m,k] in Indices G & [i,j] in Indices G holds
( m = i & k = j )
let G be Go-board; ( x = G * (m,k) & x = G * (i,j) & [m,k] in Indices G & [i,j] in Indices G implies ( m = i & k = j ) )
assume that
A1:
x = G * (m,k)
and
A2:
x = G * (i,j)
and
A3:
[m,k] in Indices G
and
A4:
[i,j] in Indices G
; ( m = i & k = j )
A5:
( len (Line (G,m)) = width G & dom (Line (G,m)) = Seg (len (Line (G,m))) )
by FINSEQ_1:def 3, MATRIX_0:def 7;
A6:
Indices G = [:(dom G),(Seg (width G)):]
by MATRIX_0:def 4;
then A7:
k in Seg (width G)
by A3, ZFMISC_1:87;
then
x = (Line (G,m)) . k
by A1, MATRIX_0:def 7;
then A8:
x in rng (Line (G,m))
by A7, A5, FUNCT_1:def 3;
A9:
( len (Col (G,k)) = len G & dom (Col (G,k)) = Seg (len (Col (G,k))) )
by FINSEQ_1:def 3, MATRIX_0:def 8;
A10:
( len (Line (G,i)) = width G & dom (Line (G,i)) = Seg (len (Line (G,i))) )
by FINSEQ_1:def 3, MATRIX_0:def 7;
A11:
( len (Col (G,j)) = len G & dom (Col (G,j)) = Seg (len (Col (G,j))) )
by FINSEQ_1:def 3, MATRIX_0:def 8;
A12:
dom G = Seg (len G)
by FINSEQ_1:def 3;
A13:
j in Seg (width G)
by A4, A6, ZFMISC_1:87;
then
x = (Line (G,i)) . j
by A2, MATRIX_0:def 7;
then A14:
x in rng (Line (G,i))
by A13, A10, FUNCT_1:def 3;
A15:
i in dom G
by A4, A6, ZFMISC_1:87;
then
x = (Col (G,j)) . i
by A2, MATRIX_0:def 8;
then A16:
x in rng (Col (G,j))
by A15, A12, A11, FUNCT_1:def 3;
A17:
m in dom G
by A3, A6, ZFMISC_1:87;
then
x = (Col (G,k)) . m
by A1, MATRIX_0:def 8;
then
x in rng (Col (G,k))
by A17, A12, A9, FUNCT_1:def 3;
hence
( m = i & k = j )
by A17, A15, A7, A13, A8, A14, A16, Th2, Th3; verum