:: deftheorem Def17 defines IDEA_P_F IDEA_1:def 17 :
for r, lk being Nat
for n being non zero Nat
for Key being Matrix of lk,6,NAT
for b₅ being FinSequence holds
( b₅ = IDEA_P_F (Key,n,r) iff ( len b₅ = r & ( for i being Nat st i in dom b₅ holds
b₅ . i = IDEA_P ((Line (Key,i)),n) ) ) );