for n being non zero Nat
for lk being Nat
for Key being Matrix of lk,6,NAT
for k being Nat st k <> 0 holds
IDEA_Q_F (Key,n,k) is FuncSequence of MESSAGES , MESSAGES