theorem :: FINSEQ_5:79

for D being non empty set holds Rev (<*> D) = <*> D ;