begin
definition
let X be
set ;
let b be
bag of
X;
end;
begin
Lm1:
for L being non empty doubleLoopStr
for p being Polynomial of {},L ex a being Element of L st p = {(EmptyBag {})} --> a
begin
begin
Lm2:
for X being set
for L being non empty ZeroStr
for c being ConstPoly of X,L holds
( term c = EmptyBag X & coefficient c = c . (EmptyBag X) )
Lm3:
for X being set
for L being non empty ZeroStr holds (0. L) | (X,L) = 0_ (X,L)
begin
Lm4:
for n being Ordinal
for L being non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive left_zeroed doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval (((a | (n,L)) *' p),x) = a * (eval (p,x))
Lm5:
for n being Ordinal
for L being non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive left_zeroed doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval ((p *' (a | (n,L))),x) = (eval (p,x)) * a