let p be FinSequence; 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; ( 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
; (((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
;
verum