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