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

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

A1: now :: thesis: for x being object st x in A holds

|.(<*> A).| . x = 0

dom |.(<*> A).| = A
by Th28;|.(<*> 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;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

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