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