for n being non zero Nat
for lk being Nat
for Key being Matrix of lk,6,NAT
for r being Nat holds
( rng (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) c= MESSAGES & dom (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) = MESSAGES )