let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: 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

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

( A = the carrier of (Polynom-Ring L) & Polynom-Algebra L = GenAlg A ) by Def6;

then A2: the carrier of (Polynom-Algebra L) = the carrier of (Polynom-Ring L) by Th21, Th22;

A3: the carrier of (Polynom-Algebra L) c= the carrier of (Formal-Series L) by A1, Def3;

A4: for x being Element of (Polynom-Algebra L)

for y being Element of (Polynom-Ring L) holds the addF of (Polynom-Algebra L) . (x,y) = the addF of (Polynom-Ring L) . (x,y)

A6: 1. (Polynom-Algebra L) = 1. (Formal-Series L) by A1, Def3

.= 1_. L by Def2

.= 1. (Polynom-Ring L) by POLYNOM3:def 10 ;

0. (Polynom-Algebra L) = 0. (Formal-Series L) by A1, Def3

.= 0_. L by Def2

.= 0. (Polynom-Ring L) by POLYNOM3:def 10 ;

hence 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 by A2, A4, A5, A6, BINOP_1:2; :: thesis: verum

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

( A = the carrier of (Polynom-Ring L) & Polynom-Algebra L = GenAlg A ) by Def6;

then A2: the carrier of (Polynom-Algebra L) = the carrier of (Polynom-Ring L) by Th21, Th22;

A3: the carrier of (Polynom-Algebra L) c= the carrier of (Formal-Series L) by A1, Def3;

A4: for x being Element of (Polynom-Algebra L)

for y being Element of (Polynom-Ring L) holds the addF of (Polynom-Algebra L) . (x,y) = the addF of (Polynom-Ring L) . (x,y)

proof

let x be Element of (Polynom-Algebra L); :: thesis: for y being Element of (Polynom-Ring L) holds the addF of (Polynom-Algebra L) . (x,y) = the addF of (Polynom-Ring L) . (x,y)

let y be Element of (Polynom-Ring L); :: thesis: the addF of (Polynom-Algebra L) . (x,y) = the addF of (Polynom-Ring L) . (x,y)

reconsider y1 = y as Element of (Polynom-Algebra L) by A1, Th21, Th22;

reconsider y9 = y1 as Element of (Formal-Series L) by A1, TARSKI:def 3;

reconsider x9 = x as Element of (Formal-Series L) by A3;

reconsider p = x as AlgSequence of L by A2, POLYNOM3:def 10;

reconsider x1 = x as Element of (Polynom-Ring L) by A1, Th21, Th22;

reconsider q = y as AlgSequence of L by POLYNOM3:def 10;

thus the addF of (Polynom-Algebra L) . (x,y) = x + y1

.= x9 + y9 by A1, Th15

.= p + q by Def2

.= x1 + y by POLYNOM3:def 10

.= the addF of (Polynom-Ring L) . (x,y) ; :: thesis: verum

end;let y be Element of (Polynom-Ring L); :: thesis: the addF of (Polynom-Algebra L) . (x,y) = the addF of (Polynom-Ring L) . (x,y)

reconsider y1 = y as Element of (Polynom-Algebra L) by A1, Th21, Th22;

reconsider y9 = y1 as Element of (Formal-Series L) by A1, TARSKI:def 3;

reconsider x9 = x as Element of (Formal-Series L) by A3;

reconsider p = x as AlgSequence of L by A2, POLYNOM3:def 10;

reconsider x1 = x as Element of (Polynom-Ring L) by A1, Th21, Th22;

reconsider q = y as AlgSequence of L by POLYNOM3:def 10;

thus the addF of (Polynom-Algebra L) . (x,y) = x + y1

.= x9 + y9 by A1, Th15

.= p + q by Def2

.= x1 + y by POLYNOM3:def 10

.= the addF of (Polynom-Ring L) . (x,y) ; :: thesis: verum

now :: thesis: for x being Element of (Polynom-Algebra L)

for y being Element of (Polynom-Ring L) holds the multF of (Polynom-Algebra L) . (x,y) = the multF of (Polynom-Ring L) . (x,y)

then A5:
the multF of (Polynom-Algebra L) = the multF of (Polynom-Ring L)
by A2, BINOP_1:2;for y being Element of (Polynom-Ring L) holds the multF of (Polynom-Algebra L) . (x,y) = the multF of (Polynom-Ring L) . (x,y)

let x be Element of (Polynom-Algebra L); :: thesis: for y being Element of (Polynom-Ring L) holds the multF of (Polynom-Algebra L) . (x,y) = the multF of (Polynom-Ring L) . (x,y)

let y be Element of (Polynom-Ring L); :: thesis: the multF of (Polynom-Algebra L) . (x,y) = the multF of (Polynom-Ring L) . (x,y)

reconsider y1 = y as Element of (Polynom-Algebra L) by A1, Th21, Th22;

reconsider y9 = y1 as Element of (Formal-Series L) by A1, TARSKI:def 3;

reconsider x9 = x as Element of (Formal-Series L) by A3;

reconsider p = x as AlgSequence of L by A2, POLYNOM3:def 10;

reconsider x1 = x as Element of (Polynom-Ring L) by A1, Th21, Th22;

reconsider q = y as AlgSequence of L by POLYNOM3:def 10;

thus the multF of (Polynom-Algebra L) . (x,y) = x * y1

.= x9 * y9 by A1, Th16

.= p *' q by Def2

.= x1 * y by POLYNOM3:def 10

.= the multF of (Polynom-Ring L) . (x,y) ; :: thesis: verum

end;let y be Element of (Polynom-Ring L); :: thesis: the multF of (Polynom-Algebra L) . (x,y) = the multF of (Polynom-Ring L) . (x,y)

reconsider y1 = y as Element of (Polynom-Algebra L) by A1, Th21, Th22;

reconsider y9 = y1 as Element of (Formal-Series L) by A1, TARSKI:def 3;

reconsider x9 = x as Element of (Formal-Series L) by A3;

reconsider p = x as AlgSequence of L by A2, POLYNOM3:def 10;

reconsider x1 = x as Element of (Polynom-Ring L) by A1, Th21, Th22;

reconsider q = y as AlgSequence of L by POLYNOM3:def 10;

thus the multF of (Polynom-Algebra L) . (x,y) = x * y1

.= x9 * y9 by A1, Th16

.= p *' q by Def2

.= x1 * y by POLYNOM3:def 10

.= the multF of (Polynom-Ring L) . (x,y) ; :: thesis: verum

A6: 1. (Polynom-Algebra L) = 1. (Formal-Series L) by A1, Def3

.= 1_. L by Def2

.= 1. (Polynom-Ring L) by POLYNOM3:def 10 ;

0. (Polynom-Algebra L) = 0. (Formal-Series L) by A1, Def3

.= 0_. L by Def2

.= 0. (Polynom-Ring L) by POLYNOM3:def 10 ;

hence 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 by A2, A4, A5, A6, BINOP_1:2; :: thesis: verum