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