let f be FinSequence of (TOP-REAL 2); :: thesis: for i, n, m, k being Element of NAT
for G being Go-board st rng f misses rng (Col G,i) & f /. n = G * m,k & n in dom f & m in dom G holds
i <> k
let i, n, m, k be Element of NAT ; :: thesis: for G being Go-board st rng f misses rng (Col G,i) & f /. n = G * m,k & n in dom f & m in dom G holds
i <> k
let G be Go-board; :: thesis: ( rng f misses rng (Col G,i) & f /. n = G * m,k & n in dom f & m in dom G implies i <> k )
assume that
A1: (rng f) /\ (rng (Col G,i)) = {} and
A2: f /. n = G * m,k and
A3: n in dom f and
A4: m in dom G and
A5: i = k ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
f . n = G * m,k by A2, A3, PARTFUN1:def 8;
then A6: G * m,i in rng f by A3, A5, FUNCT_1:def 5;
( dom G = Seg (len G) & dom (Col G,i) = Seg (len (Col G,i)) & len (Col G,i) = len G & (Col G,i) . m = G * m,i ) by A4, FINSEQ_1:def 3, MATRIX_1:def 9;
then G * m,i in rng (Col G,i) by A4, FUNCT_1:def 5;
hence contradiction by A1, A6, XBOOLE_0:def 4; :: thesis: verum