theorem Th40: :: IDEA_1:40

for n being non zero Nat
for lk being Nat
for Key being Matrix of lk,6,NAT
for k being Nat st k <> 0 holds
IDEA_P_F (Key,n,k) is FuncSequence of MESSAGES , MESSAGES