let p be FinSequence; :: thesis: for m, n being Nat st m <= n & n <= len p holds
(((1,m) -cut p) ^ (((m + 1),n) -cut p)) ^ (((n + 1),(len p)) -cut p) = p
let m, n be Nat; :: thesis: ( m <= n & n <= len p implies (((1,m) -cut p) ^ (((m + 1),n) -cut p)) ^ (((n + 1),(len p)) -cut p) = p )
assume that
A1: m <= n and
A2: n <= len p ; :: thesis: (((1,m) -cut p) ^ (((m + 1),n) -cut p)) ^ (((n + 1),(len p)) -cut p) = p
set cp3 = ((n + 1),(len p)) -cut p;
set cp2 = ((m + 1),n) -cut p;
set cp1 = (1,m) -cut p;
A3: 0 + 1 = 1 ;
hence (((1,m) -cut p) ^ (((m + 1),n) -cut p)) ^ (((n + 1),(len p)) -cut p) = ((1,n) -cut p) ^ (((n + 1),(len p)) -cut p) by A1, A2, Th8
.= (1,(len p)) -cut p by A2, A3, Th8
.= p by Th7 ;
:: thesis: verum