let X be set ; 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 ; 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; ( (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; for b being bag of X st b <> UnitBag x holds
(1_1 (x,L)) . b = 0. L
let b be bag of X; ( b <> UnitBag x implies (1_1 (x,L)) . b = 0. L )
assume
b <> UnitBag x
; (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
;
verum