let G be Go-board; :: thesis: for f being non empty FinSequence of (TOP-REAL 2) st len f >= 2 & f is_sequence_on G holds
not f is constant
let f be non empty FinSequence of (TOP-REAL 2); :: thesis: ( len f >= 2 & f is_sequence_on G implies not f is constant )
assume that
A1: len f >= 2 and
A2: f is_sequence_on G ; :: thesis: not f is constant
assume A3: for n, m being Element of NAT st n in dom f & m in dom f holds
f . n = f . m ; :: according to GOBOARD1:def 2 :: thesis: contradiction
1 <= len f by A1, XXREAL_0:2;
then A4: 1 in dom f by FINSEQ_3:27;
then consider i1, j1 being Element of NAT such that
A5: [i1,j1] in Indices G and
A6: f /. 1 = G * i1,j1 by A2, GOBOARD1:def 11;
A7: 1 + 1 in dom f by A1, FINSEQ_3:27;
then consider i2, j2 being Element of NAT such that
A8: [i2,j2] in Indices G and
A9: f /. 2 = G * i2,j2 by A2, GOBOARD1:def 11;
f /. 1 = f . 1 by A4, PARTFUN1:def 8
.= f . 2 by A3, A4, A7
.= f /. 2 by A7, PARTFUN1:def 8 ;
then ( i1 = i2 & j1 = j2 ) by A5, A6, A8, A9, GOBOARD1:21;
then A10: ( abs (i1 - i2) = 0 & abs (j1 - j2) = 0 ) by ABSVALUE:7;
(abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A2, A4, A5, A6, A7, A8, A9, GOBOARD1:def 11;
hence contradiction by A10; :: thesis: verum