let A be non empty set ; :: thesis: |.(<*> A).| = A --> 0
A1: dom |.(<*> A).| = A by Th29;

now

let x be set ; :: thesis: ( x in A implies |.(<*> A).| . x = 0 )
assume x in A ; :: thesis: |.(<*> A).| . x = 0
then reconsider a = x as Element of A ;
thus |.(<*> A).| . x = card (dom ({a} | {} )) by Def7
.= 0 by CARD_1:47, RELAT_1:60, RELAT_1:138 ; :: thesis: verum

end;

hence |.(<*> A).| = A --> 0 by A1, FUNCOP_1:17; :: thesis: verum