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

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