theorem Th80: :: FINSEQ_6:80

for k being Nat
for D being non empty set holds (<*> D) /^ k = <*> D