let X be set ; :: thesis: for L being non empty 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 empty 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 24
.= Bags X by FUNCOP_1:19 ;
hence (1_1 x,L) . (UnitBag x) = 1_ L by FUNCT_7:33; :: 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:34
.= 0. L by POLYNOM1:81 ;
:: thesis: verum