for m being FinSequence of NAT st len m >= 4 holds
IDEAoperationC (IDEAoperationC m) = m