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 /. m in rng (Col (G,(width G))) holds
(f | m) /. (len (f | m)) in rng (Col (G,(width G)))
let m be Element of NAT ; :: thesis: for G being Go-board st m in dom f & f /. m in rng (Col (G,(width G))) holds
(f | m) /. (len (f | m)) in rng (Col (G,(width G)))
let G be Go-board; :: thesis: ( m in dom f & f /. m in rng (Col (G,(width G))) implies (f | m) /. (len (f | m)) in rng (Col (G,(width G))) )
assume that
A1: m in dom f and
A2: f /. m in rng (Col (G,(width G))) ; :: thesis: (f | m) /. (len (f | m)) in rng (Col (G,(width G)))
m <= len f by A1, FINSEQ_3:25;
then A3: len (f | m) = m by FINSEQ_1:59;
1 <= m by A1, FINSEQ_3:25;
then m in Seg m by FINSEQ_1:1;
hence (f | m) /. (len (f | m)) in rng (Col (G,(width G))) by A1, A2, A3, FINSEQ_4:71; :: thesis: verum