let m, i, j, k be Nat; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum

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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum