let p be FinSequence; :: thesis: for m being Element of NAT st 1 <= m & m <= len p holds
m,m -cut p = <*(p . m)*>
let m be Element of NAT ; :: thesis: ( 1 <= m & m <= len p implies m,m -cut p = <*(p . m)*> )
assume that
A1: 1 <= m and
A2: m <= len p ; :: thesis: m,m -cut p = <*(p . m)*>
set mp = m,m -cut p;
A3: (len (m,m -cut p)) + m = m + 1 by A1, A2, Def1;
then (m,m -cut p) . (0 + 1) = p . (m + 0 ) by A1, A2, Def1
.= p . m ;
hence m,m -cut p = <*(p . m)*> by A3, FINSEQ_1:57; :: thesis: verum