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

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