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