:: deftheorem Def18 defines IDEA_Q_F IDEA_1:def 18 :
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_Q_F (Key,n,r) iff ( len b₅ = r & ( for i being Nat st i in dom b₅ holds
b₅ . i = IDEA_Q ((Line (Key,((r -' i) + 1))),n) ) ) );