let f be FinSequence of (TOP-REAL 2); :: thesis: for m being Element of NAT
for G being Go-board st m in dom f & f /. 1 in rng (Col G,1) holds
(f | m) /. 1 in rng (Col G,1)
let m be Element of NAT ; :: thesis: for G being Go-board st m in dom f & f /. 1 in rng (Col G,1) holds
(f | m) /. 1 in rng (Col G,1)
let G be Go-board; :: thesis: ( m in dom f & f /. 1 in rng (Col G,1) implies (f | m) /. 1 in rng (Col G,1) )
assume A1: ( m in dom f & f /. 1 in rng (Col G,1) ) ; :: thesis: (f | m) /. 1 in rng (Col G,1)
then 1 <= m by FINSEQ_3:27;
then 1 in Seg m by FINSEQ_1:3;
hence (f | m) /. 1 in rng (Col G,1) by A1, FINSEQ_4:86; :: thesis: verum