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

A1: now :: thesis: for x being object st x in A holds
|.(<*> A).| . x = 0

let x be object ; :: 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:27, RELAT_1:38, RELAT_1:107 ; :: thesis: verum

end;

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