begin
begin
begin
begin
Lm1:
for L being non empty addLoopStr
for p, q being sequence of L holds p - q = p + (- q)
begin
definition
let L be non
empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;
existence
ex b1 being non empty strict doubleLoopStr st
( ( for x being set holds
( x in the carrier of b1 iff x is Polynomial of L ) ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. b1 = 0_. L & 1. b1 = 1_. L )
uniqueness
for b1, b2 being non empty strict doubleLoopStr st ( for x being set holds
( x in the carrier of b1 iff x is Polynomial of L ) ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. b1 = 0_. L & 1. b1 = 1_. L & ( for x being set holds
( x in the carrier of b2 iff x is Polynomial of L ) ) & ( for x, y being Element of b2
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b2
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. b2 = 0_. L & 1. b2 = 1_. L holds
b1 = b2
end;