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