let I be set ; :: thesis: for MSS being ManySortedSet of I holds (MSS # ) . (<*> I) = {{} }
let MSS be ManySortedSet of I; :: thesis: (MSS # ) . (<*> I) = {{} }
reconsider eI = <*> I as Element of I * by FINSEQ_1:66;
thus (MSS # ) . (<*> I) = product (MSS * eI) by PBOOLE:def 19
.= {{} } by CARD_3:19 ; :: thesis: verum