for n being non zero Nat
for lk being Nat
for Key being Matrix of lk,6,NAT
for k being Nat holds IDEA_P_F (Key,n,k) is FuncSeq-like FinSequence