let p be FinSequence; :: thesis: for m being Element of NAT st m <= len p holds
(1,m -cut p) ^ ((m + 1),(len p) -cut p) = p
let m be Element of NAT ; :: thesis: ( m <= len p implies (1,m -cut p) ^ ((m + 1),(len p) -cut p) = p )
set cp1 = 1,m -cut p;
set cpm = (m + 1),(len p) -cut p;
A1: 0 + 1 = 1 ;
assume m <= len p ; :: thesis: (1,m -cut p) ^ ((m + 1),(len p) -cut p) = p
hence (1,m -cut p) ^ ((m + 1),(len p) -cut p) = 1,(len p) -cut p by A1, Th8
.= p by Th7 ;
:: thesis: verum