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 ;
A6: Indices G = [:(dom G),(Seg ()):] by MATRIX_0:def 4;
then A7: k in Seg () by ;
then x = (Line (G,m)) . k by ;
then A8: x in rng (Line (G,m)) by ;
A9: ( len (Col (G,k)) = len G & dom (Col (G,k)) = Seg (len (Col (G,k))) ) by ;
A10: ( len (Line (G,i)) = width G & dom (Line (G,i)) = Seg (len (Line (G,i))) ) by ;
A11: ( len (Col (G,j)) = len G & dom (Col (G,j)) = Seg (len (Col (G,j))) ) by ;
A12: dom G = Seg (len G) by FINSEQ_1:def 3;
A13: j in Seg () by ;
then x = (Line (G,i)) . j by ;
then A14: x in rng (Line (G,i)) by ;
A15: i in dom G by ;
then x = (Col (G,j)) . i by ;
then A16: x in rng (Col (G,j)) by ;
A17: m in dom G by ;
then x = (Col (G,k)) . m by ;
then x in rng (Col (G,k)) by ;
hence ( m = i & k = j ) by A17, A15, A7, A13, A8, A14, A16, Th2, Th3; :: thesis: verum