let X be non empty set ; :: thesis: for x being Element of X holds
( (UnitBag x) . x = 1 & ( for y being Element of X st x <> y holds
(UnitBag x) . y = 0 ) )
let x be Element of X; :: thesis: ( (UnitBag x) . x = 1 & ( for y being Element of X st x <> y holds
(UnitBag x) . y = 0 ) )
A1: dom (X --> 0 ) = X by FUNCOP_1:19;
thus (UnitBag x) . x = ((X --> 0 ) +* x,1) . x by PRE_POLY:def 13
.= 1 by A1, FUNCT_7:33 ; :: thesis: for y being Element of X st x <> y holds
(UnitBag x) . y = 0
let y be Element of X; :: thesis: ( x <> y implies (UnitBag x) . y = 0 )
assume x <> y ; :: thesis: (UnitBag x) . y = 0
hence (UnitBag x) . y = (EmptyBag X) . y by FUNCT_7:34
.= 0 by PRE_POLY:52 ;
:: thesis: verum