theorem Th36: :: IDEA_1:36

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 + 1)) = (IDEA_P_F (Key,n,k)) ^ <*(IDEA_P ((Line (Key,(k + 1))),n))*>