let p be FinSequence; :: thesis: for m, n being Element of 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 Element of 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