for n being non zero Nat
for M, m, k being FinSequence of NAT st M = (IDEA_P (k,n)) . m & len m >= 4 holds
( len M >= 4 & M . 1 is_expressible_by n & M . 2 is_expressible_by n & M . 3 is_expressible_by n & M . 4 is_expressible_by n )