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 ;
thus (UnitBag x) . x = ((X --> 0) +* (x,1)) . x by PBOOLE:def 3
.= 1 by A1, FUNCT_7:31 ; :: 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:32
.= 0 by PBOOLE:5 ;
:: thesis: verum