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 A1: ( m in dom f & f /. m in rng (Col G,(width G)) ) ; :: thesis: (f | m) /. (len (f | m)) in rng (Col G,(width G))
then ( 1 <= m & m <= len f ) by FINSEQ_3:27;
then ( len (f | m) = m & m in Seg m ) by FINSEQ_1:3, FINSEQ_1:80;
hence (f | m) /. (len (f | m)) in rng (Col G,(width G)) by A1, FINSEQ_4:86; :: thesis: verum