for n being non zero Nat
for lk being Nat
for Key being Matrix of lk,6,NAT
for r being Nat
for M, m being FinSequence of NAT st M = (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) . m & 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
( 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 )