let k be 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 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 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 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 Nat st
( [i,j] in Indices G & f /. k = G * (i,j) )
k in dom f by A2, FINSEQ_3:25;
then consider i, j being Nat such that
A3: ( [i,j] in Indices G & f /. k = G * (i,j) ) by A1, GOBOARD1:def 9;
take i ; :: thesis: ex j being 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