let X be set ; :: thesis: for L being non trivial unital doubleLoopStr
for x being Element of X holds
( (1_1 (x,L)) . (UnitBag x) = 1_ L & ( for b being bag of X st b <> UnitBag x holds
(1_1 (x,L)) . b = 0. L ) )
let L be non trivial unital doubleLoopStr ; :: thesis: for x being Element of X holds
( (1_1 (x,L)) . (UnitBag x) = 1_ L & ( for b being bag of X st b <> UnitBag x holds
(1_1 (x,L)) . b = 0. L ) )
let x be Element of X; :: thesis: ( (1_1 (x,L)) . (UnitBag x) = 1_ L & ( for b being bag of X st b <> UnitBag x holds
(1_1 (x,L)) . b = 0. L ) )
dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 8
.= Bags X ;
hence (1_1 (x,L)) . (UnitBag x) = 1_ L by FUNCT_7:31; :: thesis: for b being bag of X st b <> UnitBag x holds
(1_1 (x,L)) . b = 0. L
let b be bag of X; :: thesis: ( b <> UnitBag x implies (1_1 (x,L)) . b = 0. L )
assume b <> UnitBag x ; :: thesis: (1_1 (x,L)) . b = 0. L
hence (1_1 (x,L)) . b = (0_ (X,L)) . b by FUNCT_7:32
.= 0. L by POLYNOM1:22 ;
:: thesis: verum