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

(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