theorem Th5: :: MATRIX_7:5

for D being non empty set
for f being FinSequence of D
for k2 being Nat st 1 <= k2 & k2 < len f holds
f = (mid (f,1,k2)) ^ (mid (f,(k2 + 1),(len f)))