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:56;
then dom ({a} |` (<*> A)) = {} ;
hence |.(<*> A).| . a = 0 by Def7, CARD_1:27; :: thesis: verum