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