:: deftheorem Def16 defines IDEA_Q IDEA_1:def 16 :
for n being non zero Nat
for k being FinSequence of NAT
for b₃ being Function of MESSAGES,MESSAGES holds
( b₃ = IDEA_Q (k,n) iff for m being FinSequence of NAT holds b₃ . m = IDEAoperationB ((IDEAoperationA ((IDEAoperationC m),k,n)),k,n) );