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 POLYNOM1:def 15
.= 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 A2: x <> y ; :: thesis: (UnitBag x) . y = 0
thus (UnitBag x) . y = (EmptyBag X) . y by A2, FUNCT_7:34
.= 0 by POLYNOM1:56 ; :: thesis: verum