for n being Nat
for m being FinSequence of NAT st 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 holds
( (IDEAoperationC m) . 1 is_expressible_by n & (IDEAoperationC m) . 2 is_expressible_by n & (IDEAoperationC m) . 3 is_expressible_by n & (IDEAoperationC m) . 4 is_expressible_by n )