theorem Th39: :: IDEA_1:39

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) is FuncSeq-like FinSequence