for n being non zero Nat
for lk being Nat
for Key being Matrix of lk,6,NAT
for k being Nat holds IDEA_Q_F (Key,n,(k + 1)) = <*(IDEA_Q ((Line (Key,(k + 1))),n))*> ^ (IDEA_Q_F (Key,n,k))