:: by Ewa Gr\c{a}dzka

::

:: Received February 24, 2001

:: Copyright (c) 2001-2016 Association of Mizar Users

definition

let F be 1-sorted ;

attr c_{2} is strict ;

struct AlgebraStr over F -> doubleLoopStr , ModuleStr over F;

aggr AlgebraStr(# carrier, addF, multF, ZeroF, OneF, lmult #) -> AlgebraStr over F;

end;
attr c

struct AlgebraStr over F -> doubleLoopStr , ModuleStr over F;

aggr AlgebraStr(# carrier, addF, multF, ZeroF, OneF, lmult #) -> AlgebraStr over F;

registration

let L be non empty doubleLoopStr ;

existence

ex b_{1} being AlgebraStr over L st

( b_{1} is strict & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

definition

let L be non empty doubleLoopStr ;

let A be non empty AlgebraStr over L;

end;
let A be non empty AlgebraStr over L;

attr A is mix-associative means :: POLYALG1:def 1

for a being Element of L

for x, y being Element of A holds a * (x * y) = (a * x) * y;

for a being Element of L

for x, y being Element of A holds a * (x * y) = (a * x) * y;

:: deftheorem defines mix-associative POLYALG1:def 1 :

for L being non empty doubleLoopStr

for A being non empty AlgebraStr over L holds

( A is mix-associative iff for a being Element of L

for x, y being Element of A holds a * (x * y) = (a * x) * y );

for L being non empty doubleLoopStr

for A being non empty AlgebraStr over L holds

( A is mix-associative iff for a being Element of L

for x, y being Element of A holds a * (x * y) = (a * x) * y );

registration

let L be non empty doubleLoopStr ;

ex b_{1} being non empty AlgebraStr over L st

( b_{1} is unital & b_{1} is distributive & b_{1} is vector-distributive & b_{1} is scalar-distributive & b_{1} is scalar-associative & b_{1} is scalar-unital & b_{1} is mix-associative )

end;
cluster non empty distributive vector-distributive scalar-distributive scalar-associative scalar-unital unital mix-associative for AlgebraStr over L;

existence ex b

( b

proof end;

definition

let L be non empty doubleLoopStr ;

mode Algebra of L is non empty distributive vector-distributive scalar-distributive scalar-associative scalar-unital unital mix-associative AlgebraStr over L;

end;
mode Algebra of L is non empty distributive vector-distributive scalar-distributive scalar-associative scalar-unital unital mix-associative AlgebraStr over L;

definition

let L be non empty doubleLoopStr ;

ex b_{1} being non empty strict AlgebraStr over L st

( ( for x being set holds

( x in the carrier of b_{1} iff x is sequence of L ) ) & ( for x, y being Element of b_{1}

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b_{1}

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & ( for a being Element of L

for x being Element of b_{1}

for p being sequence of L st x = p holds

a * x = a * p ) & 0. b_{1} = 0_. L & 1. b_{1} = 1_. L )

for b_{1}, b_{2} being non empty strict AlgebraStr over L st ( for x being set holds

( x in the carrier of b_{1} iff x is sequence of L ) ) & ( for x, y being Element of b_{1}

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b_{1}

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & ( for a being Element of L

for x being Element of b_{1}

for p being sequence of L st x = p holds

a * x = a * p ) & 0. b_{1} = 0_. L & 1. b_{1} = 1_. L & ( for x being set holds

( x in the carrier of b_{2} iff x is sequence of L ) ) & ( for x, y being Element of b_{2}

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b_{2}

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & ( for a being Element of L

for x being Element of b_{2}

for p being sequence of L st x = p holds

a * x = a * p ) & 0. b_{2} = 0_. L & 1. b_{2} = 1_. L holds

b_{1} = b_{2}

end;
func Formal-Series L -> non empty strict AlgebraStr over L means :Def2: :: POLYALG1:def 2

( ( for x being set holds

( x in the carrier of it iff x is sequence of L ) ) & ( for x, y being Element of it

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of it

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & ( for a being Element of L

for x being Element of it

for p being sequence of L st x = p holds

a * x = a * p ) & 0. it = 0_. L & 1. it = 1_. L );

existence ( ( for x being set holds

( x in the carrier of it iff x is sequence of L ) ) & ( for x, y being Element of it

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of it

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & ( for a being Element of L

for x being Element of it

for p being sequence of L st x = p holds

a * x = a * p ) & 0. it = 0_. L & 1. it = 1_. L );

ex b

( ( for x being set holds

( x in the carrier of b

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & ( for a being Element of L

for x being Element of b

for p being sequence of L st x = p holds

a * x = a * p ) & 0. b

proof end;

uniqueness for b

( x in the carrier of b

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & ( for a being Element of L

for x being Element of b

for p being sequence of L st x = p holds

a * x = a * p ) & 0. b

( x in the carrier of b

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & ( for a being Element of L

for x being Element of b

for p being sequence of L st x = p holds

a * x = a * p ) & 0. b

b

proof end;

:: deftheorem Def2 defines Formal-Series POLYALG1:def 2 :

for L being non empty doubleLoopStr

for b_{2} being non empty strict AlgebraStr over L holds

( b_{2} = Formal-Series L iff ( ( for x being set holds

( x in the carrier of b_{2} iff x is sequence of L ) ) & ( for x, y being Element of b_{2}

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b_{2}

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & ( for a being Element of L

for x being Element of b_{2}

for p being sequence of L st x = p holds

a * x = a * p ) & 0. b_{2} = 0_. L & 1. b_{2} = 1_. L ) );

for L being non empty doubleLoopStr

for b

( b

( x in the carrier of b

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & ( for a being Element of L

for x being Element of b

for p being sequence of L st x = p holds

a * x = a * p ) & 0. b

registration
end;

registration

let L be non empty add-associative doubleLoopStr ;

coherence

Formal-Series L is add-associative

end;
coherence

Formal-Series L is add-associative

proof end;

registration

let L be non empty right_zeroed doubleLoopStr ;

coherence

Formal-Series L is right_zeroed

end;
coherence

Formal-Series L is right_zeroed

proof end;

registration

let L be non empty right_complementable add-associative right_zeroed doubleLoopStr ;

coherence

Formal-Series L is right_complementable

end;
coherence

Formal-Series L is right_complementable

proof end;

registration

let L be non empty Abelian add-associative right_zeroed commutative doubleLoopStr ;

coherence

Formal-Series L is commutative

end;
coherence

Formal-Series L is commutative

proof end;

registration

let L be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

coherence

Formal-Series L is associative

end;
coherence

Formal-Series L is associative

proof end;

registration

ex b_{1} being non empty doubleLoopStr st

( b_{1} is add-associative & b_{1} is associative & b_{1} is right_zeroed & b_{1} is left_zeroed & b_{1} is well-unital & b_{1} is right_complementable & b_{1} is distributive )
end;

cluster non empty right_complementable left_zeroed well-unital distributive add-associative right_zeroed associative for doubleLoopStr ;

existence ex b

( b

proof end;

theorem Th4: :: POLYALG1:4

for D being non empty set

for f being non empty FinSequence of D holds f = <*(f . 1)*> ^ (Del (f,1))

for f being non empty FinSequence of D holds f = <*(f . 1)*> ^ (Del (f,1))

proof end;

theorem Th5: :: POLYALG1:5

for L being non empty right_complementable left-distributive well-unital add-associative right_zeroed doubleLoopStr

for p being sequence of L holds (1_. L) *' p = p

for p being sequence of L holds (1_. L) *' p = p

proof end;

Lm1: now :: thesis: for L being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr

for x, e being Element of (Formal-Series L) st e = 1_. L holds

( x * e = x & e * x = x )

for x, e being Element of (Formal-Series L) st e = 1_. L holds

( x * e = x & e * x = x )

let L be non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for x, e being Element of (Formal-Series L) st e = 1_. L holds

( x * e = x & e * x = x )

set F = Formal-Series L;

let x, e be Element of (Formal-Series L); :: thesis: ( e = 1_. L implies ( x * e = x & e * x = x ) )

reconsider a = x, b = e as sequence of L by Def2;

assume A1: e = 1_. L ; :: thesis: ( x * e = x & e * x = x )

thus x * e = a *' b by Def2

.= x by A1, POLYNOM3:35 ; :: thesis: e * x = x

thus e * x = b *' a by Def2

.= x by A1, Th5 ; :: thesis: verum

end;
( x * e = x & e * x = x )

set F = Formal-Series L;

let x, e be Element of (Formal-Series L); :: thesis: ( e = 1_. L implies ( x * e = x & e * x = x ) )

reconsider a = x, b = e as sequence of L by Def2;

assume A1: e = 1_. L ; :: thesis: ( x * e = x & e * x = x )

thus x * e = a *' b by Def2

.= x by A1, POLYNOM3:35 ; :: thesis: e * x = x

thus e * x = b *' a by Def2

.= x by A1, Th5 ; :: thesis: verum

registration

let L be non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ;

coherence

Formal-Series L is well-unital

end;
coherence

Formal-Series L is well-unital

proof end;

registration

let L be non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr ;

coherence

Formal-Series L is right-distributive

Formal-Series L is left-distributive

end;
coherence

Formal-Series L is right-distributive

proof end;

coherence Formal-Series L is left-distributive

proof end;

theorem Th6: :: POLYALG1:6

for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr

for a being Element of L

for p, q being sequence of L holds a * (p + q) = (a * p) + (a * q)

for a being Element of L

for p, q being sequence of L holds a * (p + q) = (a * p) + (a * q)

proof end;

theorem Th7: :: POLYALG1:7

for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr

for a, b being Element of L

for p being sequence of L holds (a + b) * p = (a * p) + (b * p)

for a, b being Element of L

for p being sequence of L holds (a + b) * p = (a * p) + (b * p)

proof end;

theorem Th8: :: POLYALG1:8

for L being non empty associative doubleLoopStr

for a, b being Element of L

for p being sequence of L holds (a * b) * p = a * (b * p)

for a, b being Element of L

for p being sequence of L holds (a * b) * p = a * (b * p)

proof end;

theorem Th9: :: POLYALG1:9

for L being non empty well-unital associative doubleLoopStr

for p being sequence of L holds (1. L) * p = p

for p being sequence of L holds (1. L) * p = p

proof end;

registration

let L be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

( Formal-Series L is vector-distributive & Formal-Series L is scalar-distributive & Formal-Series L is scalar-associative & Formal-Series L is scalar-unital )

end;
cluster Formal-Series L -> non empty vector-distributive scalar-distributive scalar-associative scalar-unital strict ;

coherence ( Formal-Series L is vector-distributive & Formal-Series L is scalar-distributive & Formal-Series L is scalar-associative & Formal-Series L is scalar-unital )

proof end;

theorem Th10: :: POLYALG1:10

for L being non empty right_complementable left_zeroed distributive Abelian add-associative right_zeroed associative doubleLoopStr

for a being Element of L

for p, q being sequence of L holds a * (p *' q) = (a * p) *' q

for a being Element of L

for p, q being sequence of L holds a * (p *' q) = (a * p) *' q

proof end;

registration

let L be non empty right_complementable left_zeroed distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

coherence

Formal-Series L is mix-associative

end;
coherence

Formal-Series L is mix-associative

proof end;

definition

let L be 1-sorted ;

let A be AlgebraStr over L;

ex b_{1} being AlgebraStr over L st

( the carrier of b_{1} c= the carrier of A & 1. b_{1} = 1. A & 0. b_{1} = 0. A & the addF of b_{1} = the addF of A || the carrier of b_{1} & the multF of b_{1} = the multF of A || the carrier of b_{1} & the lmult of b_{1} = the lmult of A | [: the carrier of L, the carrier of b_{1}:] )

end;
let A be AlgebraStr over L;

mode Subalgebra of A -> AlgebraStr over L means :Def3: :: POLYALG1:def 3

( the carrier of it c= the carrier of A & 1. it = 1. A & 0. it = 0. A & the addF of it = the addF of A || the carrier of it & the multF of it = the multF of A || the carrier of it & the lmult of it = the lmult of A | [: the carrier of L, the carrier of it:] );

existence ( the carrier of it c= the carrier of A & 1. it = 1. A & 0. it = 0. A & the addF of it = the addF of A || the carrier of it & the multF of it = the multF of A || the carrier of it & the lmult of it = the lmult of A | [: the carrier of L, the carrier of it:] );

ex b

( the carrier of b

proof end;

:: deftheorem Def3 defines Subalgebra POLYALG1:def 3 :

for L being 1-sorted

for A, b_{3} being AlgebraStr over L holds

( b_{3} is Subalgebra of A iff ( the carrier of b_{3} c= the carrier of A & 1. b_{3} = 1. A & 0. b_{3} = 0. A & the addF of b_{3} = the addF of A || the carrier of b_{3} & the multF of b_{3} = the multF of A || the carrier of b_{3} & the lmult of b_{3} = the lmult of A | [: the carrier of L, the carrier of b_{3}:] ) );

for L being 1-sorted

for A, b

( b

theorem :: POLYALG1:12

for L being 1-sorted

for A, B, C being AlgebraStr over L st A is Subalgebra of B & B is Subalgebra of C holds

A is Subalgebra of C

for A, B, C being AlgebraStr over L st A is Subalgebra of B & B is Subalgebra of C holds

A is Subalgebra of C

proof end;

theorem :: POLYALG1:13

for L being 1-sorted

for A, B being AlgebraStr over L st A is Subalgebra of B & B is Subalgebra of A holds

AlgebraStr(# the carrier of A, the addF of A, the multF of A, the ZeroF of A, the OneF of A, the lmult of A #) = AlgebraStr(# the carrier of B, the addF of B, the multF of B, the ZeroF of B, the OneF of B, the lmult of B #)

for A, B being AlgebraStr over L st A is Subalgebra of B & B is Subalgebra of A holds

AlgebraStr(# the carrier of A, the addF of A, the multF of A, the ZeroF of A, the OneF of A, the lmult of A #) = AlgebraStr(# the carrier of B, the addF of B, the multF of B, the ZeroF of B, the OneF of B, the lmult of B #)

proof end;

theorem Th14: :: POLYALG1:14

for L being 1-sorted

for A, B being AlgebraStr over L st AlgebraStr(# the carrier of A, the addF of A, the multF of A, the ZeroF of A, the OneF of A, the lmult of A #) = AlgebraStr(# the carrier of B, the addF of B, the multF of B, the ZeroF of B, the OneF of B, the lmult of B #) holds

A is Subalgebra of B

for A, B being AlgebraStr over L st AlgebraStr(# the carrier of A, the addF of A, the multF of A, the ZeroF of A, the OneF of A, the lmult of A #) = AlgebraStr(# the carrier of B, the addF of B, the multF of B, the ZeroF of B, the OneF of B, the lmult of B #) holds

A is Subalgebra of B

proof end;

registration

let L be non empty 1-sorted ;

existence

ex b_{1} being AlgebraStr over L st

( not b_{1} is empty & b_{1} is strict )

end;
existence

ex b

( not b

proof end;

registration

let L be 1-sorted ;

let B be AlgebraStr over L;

existence

ex b_{1} being Subalgebra of B st b_{1} is strict

end;
let B be AlgebraStr over L;

existence

ex b

proof end;

registration

let L be non empty 1-sorted ;

let B be non empty AlgebraStr over L;

existence

ex b_{1} being Subalgebra of B st

( b_{1} is strict & not b_{1} is empty )

end;
let B be non empty AlgebraStr over L;

existence

ex b

( b

proof end;

definition

let L be non empty multMagma ;

let B be non empty AlgebraStr over L;

let A be Subset of B;

end;
let B be non empty AlgebraStr over L;

let A be Subset of B;

attr A is opers_closed means :Def4: :: POLYALG1:def 4

( A is linearly-closed & ( for x, y being Element of B st x in A & y in A holds

x * y in A ) & 1. B in A & 0. B in A );

( A is linearly-closed & ( for x, y being Element of B st x in A & y in A holds

x * y in A ) & 1. B in A & 0. B in A );

:: deftheorem Def4 defines opers_closed POLYALG1:def 4 :

for L being non empty multMagma

for B being non empty AlgebraStr over L

for A being Subset of B holds

( A is opers_closed iff ( A is linearly-closed & ( for x, y being Element of B st x in A & y in A holds

x * y in A ) & 1. B in A & 0. B in A ) );

for L being non empty multMagma

for B being non empty AlgebraStr over L

for A being Subset of B holds

( A is opers_closed iff ( A is linearly-closed & ( for x, y being Element of B st x in A & y in A holds

x * y in A ) & 1. B in A & 0. B in A ) );

theorem Th15: :: POLYALG1:15

for L being non empty multMagma

for B being non empty AlgebraStr over L

for A being non empty Subalgebra of B

for x, y being Element of B

for x9, y9 being Element of A st x = x9 & y = y9 holds

x + y = x9 + y9

for B being non empty AlgebraStr over L

for A being non empty Subalgebra of B

for x, y being Element of B

for x9, y9 being Element of A st x = x9 & y = y9 holds

x + y = x9 + y9

proof end;

theorem Th16: :: POLYALG1:16

for L being non empty multMagma

for B being non empty AlgebraStr over L

for A being non empty Subalgebra of B

for x, y being Element of B

for x9, y9 being Element of A st x = x9 & y = y9 holds

x * y = x9 * y9

for B being non empty AlgebraStr over L

for A being non empty Subalgebra of B

for x, y being Element of B

for x9, y9 being Element of A st x = x9 & y = y9 holds

x * y = x9 * y9

proof end;

theorem Th17: :: POLYALG1:17

for L being non empty multMagma

for B being non empty AlgebraStr over L

for A being non empty Subalgebra of B

for a being Element of L

for x being Element of B

for x9 being Element of A st x = x9 holds

a * x = a * x9

for B being non empty AlgebraStr over L

for A being non empty Subalgebra of B

for a being Element of L

for x being Element of B

for x9 being Element of A st x = x9 holds

a * x = a * x9

proof end;

theorem :: POLYALG1:18

for L being non empty multMagma

for B being non empty AlgebraStr over L

for A being non empty Subalgebra of B ex C being Subset of B st

( the carrier of A = C & C is opers_closed )

for B being non empty AlgebraStr over L

for A being non empty Subalgebra of B ex C being Subset of B st

( the carrier of A = C & C is opers_closed )

proof end;

theorem Th19: :: POLYALG1:19

for L being non empty multMagma

for B being non empty AlgebraStr over L

for A being Subset of B st A is opers_closed holds

ex C being strict Subalgebra of B st the carrier of C = A

for B being non empty AlgebraStr over L

for A being Subset of B st A is opers_closed holds

ex C being strict Subalgebra of B st the carrier of C = A

proof end;

theorem Th20: :: POLYALG1:20

for L being non empty multMagma

for B being non empty AlgebraStr over L

for A being non empty Subset of B

for X being Subset-Family of B st ( for Y being set holds

( Y in X iff ( Y c= the carrier of B & ex C being Subalgebra of B st

( Y = the carrier of C & A c= Y ) ) ) ) holds

meet X is opers_closed

for B being non empty AlgebraStr over L

for A being non empty Subset of B

for X being Subset-Family of B st ( for Y being set holds

( Y in X iff ( Y c= the carrier of B & ex C being Subalgebra of B st

( Y = the carrier of C & A c= Y ) ) ) ) holds

meet X is opers_closed

proof end;

definition

let L be non empty multMagma ;

let B be non empty AlgebraStr over L;

let A be non empty Subset of B;

ex b_{1} being non empty strict Subalgebra of B st

( A c= the carrier of b_{1} & ( for C being Subalgebra of B st A c= the carrier of C holds

the carrier of b_{1} c= the carrier of C ) )

for b_{1}, b_{2} being non empty strict Subalgebra of B st A c= the carrier of b_{1} & ( for C being Subalgebra of B st A c= the carrier of C holds

the carrier of b_{1} c= the carrier of C ) & A c= the carrier of b_{2} & ( for C being Subalgebra of B st A c= the carrier of C holds

the carrier of b_{2} c= the carrier of C ) holds

b_{1} = b_{2}

end;
let B be non empty AlgebraStr over L;

let A be non empty Subset of B;

func GenAlg A -> non empty strict Subalgebra of B means :Def5: :: POLYALG1:def 5

( A c= the carrier of it & ( for C being Subalgebra of B st A c= the carrier of C holds

the carrier of it c= the carrier of C ) );

existence ( A c= the carrier of it & ( for C being Subalgebra of B st A c= the carrier of C holds

the carrier of it c= the carrier of C ) );

ex b

( A c= the carrier of b

the carrier of b

proof end;

uniqueness for b

the carrier of b

the carrier of b

b

proof end;

:: deftheorem Def5 defines GenAlg POLYALG1:def 5 :

for L being non empty multMagma

for B being non empty AlgebraStr over L

for A being non empty Subset of B

for b_{4} being non empty strict Subalgebra of B holds

( b_{4} = GenAlg A iff ( A c= the carrier of b_{4} & ( for C being Subalgebra of B st A c= the carrier of C holds

the carrier of b_{4} c= the carrier of C ) ) );

for L being non empty multMagma

for B being non empty AlgebraStr over L

for A being non empty Subset of B

for b

( b

the carrier of b

theorem Th21: :: POLYALG1:21

for L being non empty multMagma

for B being non empty AlgebraStr over L

for A being non empty Subset of B st A is opers_closed holds

the carrier of (GenAlg A) = A

for B being non empty AlgebraStr over L

for A being non empty Subset of B st A is opers_closed holds

the carrier of (GenAlg A) = A

proof end;

definition

let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;

ex b_{1} being non empty strict AlgebraStr over L ex A being non empty Subset of (Formal-Series L) st

( A = the carrier of (Polynom-Ring L) & b_{1} = GenAlg A )

for b_{1}, b_{2} being non empty strict AlgebraStr over L st ex A being non empty Subset of (Formal-Series L) st

( A = the carrier of (Polynom-Ring L) & b_{1} = GenAlg A ) & ex A being non empty Subset of (Formal-Series L) st

( A = the carrier of (Polynom-Ring L) & b_{2} = GenAlg A ) holds

b_{1} = b_{2}
;

end;
func Polynom-Algebra L -> non empty strict AlgebraStr over L means :Def6: :: POLYALG1:def 6

ex A being non empty Subset of (Formal-Series L) st

( A = the carrier of (Polynom-Ring L) & it = GenAlg A );

existence ex A being non empty Subset of (Formal-Series L) st

( A = the carrier of (Polynom-Ring L) & it = GenAlg A );

ex b

( A = the carrier of (Polynom-Ring L) & b

proof end;

uniqueness for b

( A = the carrier of (Polynom-Ring L) & b

( A = the carrier of (Polynom-Ring L) & b

b

:: deftheorem Def6 defines Polynom-Algebra POLYALG1:def 6 :

for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr

for b_{2} being non empty strict AlgebraStr over L holds

( b_{2} = Polynom-Algebra L iff ex A being non empty Subset of (Formal-Series L) st

( A = the carrier of (Polynom-Ring L) & b_{2} = GenAlg A ) );

for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr

for b

( b

( A = the carrier of (Polynom-Ring L) & b

registration

let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;

coherence

Polynom-Ring L is Loop-like

end;
coherence

Polynom-Ring L is Loop-like

proof end;

theorem Th22: :: POLYALG1:22

for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr

for A being non empty Subset of (Formal-Series L) st A = the carrier of (Polynom-Ring L) holds

A is opers_closed

for A being non empty Subset of (Formal-Series L) st A = the carrier of (Polynom-Ring L) holds

A is opers_closed

proof end;

theorem :: POLYALG1:23

for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr holds doubleLoopStr(# the carrier of (Polynom-Algebra L), the addF of (Polynom-Algebra L), the multF of (Polynom-Algebra L), the OneF of (Polynom-Algebra L), the ZeroF of (Polynom-Algebra L) #) = Polynom-Ring L

proof end;

theorem :: POLYALG1:24

for L being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr holds 1_ (Formal-Series L) = 1_. L by Def2;