theorem :: FINSEQ_5:78

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