let p be FinSequence; :: thesis: for m being Nat st 1 <= m & m <= len p holds
(m,m) -cut p = <*(p . m)*>
let m be 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:40; :: thesis: verum