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:49;
thus (MSS #) . (<*> I) = product (MSS * eI) by FINSEQ_2:def 5
.= {{}} by CARD_3:10 ; :: thesis: verum