theorem :: FINSEQ_5:78

for D being non empty set
for i being Nat holds (<*> D) | i = <*> D ;