let k be Element of NAT ; :: thesis: for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & 1 <= k & k <= len f holds
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. k = G * i,j )
let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & 1 <= k & k <= len f holds
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. k = G * i,j )
let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G & 1 <= k & k <= len f implies ex i, j being Element of NAT st
( [i,j] in Indices G & f /. k = G * i,j ) )
assume that
A1: f is_sequence_on G and
A2: ( 1 <= k & k <= len f ) ; :: thesis: ex i, j being Element of NAT st
( [i,j] in Indices G & f /. k = G * i,j )
k in dom f by A2, FINSEQ_3:27;
then consider i, j being Element of NAT such that
A3: ( [i,j] in Indices G & f /. k = G * i,j ) by A1, GOBOARD1:def 11;
take i ; :: thesis: ex j being Element of NAT st
( [i,j] in Indices G & f /. k = G * i,j )
take j ; :: thesis: ( [i,j] in Indices G & f /. k = G * i,j )
thus ( [i,j] in Indices G & f /. k = G * i,j ) by A3; :: thesis: verum