let A be non empty set ; :: thesis: for a being Element of A holds |.(<*> A).| . a = 0
let a be Element of A; :: thesis: |.(<*> A).| . a = 0
dom ({a} | {} ) c= dom {} by FUNCT_1:89;
then dom ({a} | (<*> A)) = {} ;
hence |.(<*> A).| . a = 0 by Def7, CARD_1:47; :: thesis: verum