set n = {} ;

let L be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: Polynom-Ring ({},L) is_ringisomorph_to L

set PL = Polynom-Ring ({},L);

defpred S_{1}[ set , set ] means ex p being Polynomial of {},L st

( p = $1 & p . {} = $2 );

A1: dom (0_ ({},L)) = Bags {} by FUNCT_2:def 1;

A2: EmptyBag {} in dom ((EmptyBag {}) .--> (1_ L)) by TARSKI:def 1;

A3: for b being bag of {} holds b = {}

then reconsider i = {} as bag of {} ;

A5: for x being Element of (Polynom-Ring ({},L)) ex y being Element of L st S_{1}[x,y]

A7: for x being Element of (Polynom-Ring ({},L)) holds S_{1}[x,f . x]
from FUNCT_2:sch 3(A5);

A8: dom f = the carrier of (Polynom-Ring ({},L)) by FUNCT_2:def 1;

reconsider f = f as Function of (Polynom-Ring ({},L)),L ;

consider p being Polynomial of {},L such that

A9: p = 1_ (Polynom-Ring ({},L)) and

A10: p . {} = f . (1. (Polynom-Ring ({},L))) by A7;

A11: p = 1_ ({},L) by A9, POLYNOM1:31

.= (0_ ({},L)) +* ((EmptyBag {}),(1_ L)) by POLYNOM1:def 9 ;

for x, y being Element of (Polynom-Ring ({},L)) holds f . (x * y) = (f . x) * (f . y)

for x, y being Element of (Polynom-Ring ({},L)) holds f . (x + y) = (f . x) + (f . y)

p . i = p . (EmptyBag {}) by A3

.= ((0_ ({},L)) +* ((EmptyBag {}) .--> (1_ L))) . (EmptyBag {}) by A11, A1, FUNCT_7:def 3

.= ((EmptyBag {}) .--> (1_ L)) . (EmptyBag {}) by A2, FUNCT_4:13

.= 1_ L by FUNCOP_1:72 ;

then f is unity-preserving by A9, A10, GROUP_1:def 13;

then A33: f is RingHomomorphism by A32, A22;

A34: for u being object st u in the carrier of L holds

u in rng f

then for u being object st u in rng f holds

u in the carrier of L ;

then rng f = the carrier of L by A34, TARSKI:2;

then f is onto ;

then A42: f is RingEpimorphism by A33;

for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds

x1 = x2

then f is RingMonomorphism by A33;

then f is RingIsomorphism by A42;

hence Polynom-Ring ({},L) is_ringisomorph_to L by QUOFIELD:def 23; :: thesis: verum

let L be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: Polynom-Ring ({},L) is_ringisomorph_to L

set PL = Polynom-Ring ({},L);

defpred S

( p = $1 & p . {} = $2 );

A1: dom (0_ ({},L)) = Bags {} by FUNCT_2:def 1;

A2: EmptyBag {} in dom ((EmptyBag {}) .--> (1_ L)) by TARSKI:def 1;

A3: for b being bag of {} holds b = {}

proof

then A4:
EmptyBag {} = {}
;
let b be bag of {} ; :: thesis: b = {}

b in Bags {} by PRE_POLY:def 12;

hence b = {} by PRE_POLY:51, TARSKI:def 1; :: thesis: verum

end;b in Bags {} by PRE_POLY:def 12;

hence b = {} by PRE_POLY:51, TARSKI:def 1; :: thesis: verum

then reconsider i = {} as bag of {} ;

A5: for x being Element of (Polynom-Ring ({},L)) ex y being Element of L st S

proof

consider f being Function of the carrier of (Polynom-Ring ({},L)), the carrier of L such that
let x be Element of (Polynom-Ring ({},L)); :: thesis: ex y being Element of L st S_{1}[x,y]

reconsider p = x as Polynomial of {},L by POLYNOM1:def 11;

take p . {} ; :: thesis: ( p . {} is Element of L & S_{1}[x,p . {}] )

dom p = Bags {} by FUNCT_2:def 1;

then A6: p . {} in rng p by A4, FUNCT_1:3;

rng p c= the carrier of L by RELAT_1:def 19;

hence ( p . {} is Element of L & S_{1}[x,p . {}] )
by A6; :: thesis: verum

end;reconsider p = x as Polynomial of {},L by POLYNOM1:def 11;

take p . {} ; :: thesis: ( p . {} is Element of L & S

dom p = Bags {} by FUNCT_2:def 1;

then A6: p . {} in rng p by A4, FUNCT_1:3;

rng p c= the carrier of L by RELAT_1:def 19;

hence ( p . {} is Element of L & S

A7: for x being Element of (Polynom-Ring ({},L)) holds S

A8: dom f = the carrier of (Polynom-Ring ({},L)) by FUNCT_2:def 1;

reconsider f = f as Function of (Polynom-Ring ({},L)),L ;

consider p being Polynomial of {},L such that

A9: p = 1_ (Polynom-Ring ({},L)) and

A10: p . {} = f . (1. (Polynom-Ring ({},L))) by A7;

A11: p = 1_ ({},L) by A9, POLYNOM1:31

.= (0_ ({},L)) +* ((EmptyBag {}),(1_ L)) by POLYNOM1:def 9 ;

for x, y being Element of (Polynom-Ring ({},L)) holds f . (x * y) = (f . x) * (f . y)

proof

then A22:
f is multiplicative
by GROUP_6:def 6;
let x, y be Element of (Polynom-Ring ({},L)); :: thesis: f . (x * y) = (f . x) * (f . y)

consider p being Polynomial of {},L such that

A12: ( p = x & p . {} = f . x ) by A7;

consider q being Polynomial of {},L such that

A13: ( q = y & q . {} = f . y ) by A7;

A14: (p *' q) . {} = (p . i) * (q . i)

( pq = x * y & pq . {} = f . (x * y) ) by A7;

hence f . (x * y) = (f . x) * (f . y) by A12, A13, A14, POLYNOM1:def 11; :: thesis: verum

end;consider p being Polynomial of {},L such that

A12: ( p = x & p . {} = f . x ) by A7;

consider q being Polynomial of {},L such that

A13: ( q = y & q . {} = f . y ) by A7;

A14: (p *' q) . {} = (p . i) * (q . i)

proof

ex pq being Polynomial of {},L st
A15:
decomp (EmptyBag {}) = <*<*(EmptyBag {}),(EmptyBag {})*>*>
by PRE_POLY:73;

then A16: len (decomp (EmptyBag {})) = 1 by FINSEQ_1:39;

set z = (p . i) * (q . i);

consider s being FinSequence of the carrier of L such that

A17: (p *' q) . (EmptyBag {}) = Sum s and

A18: len s = len (decomp (EmptyBag {})) and

A19: for k being Element of NAT st k in dom s holds

ex b1, b2 being bag of {} st

( (decomp (EmptyBag {})) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by POLYNOM1:def 10;

len s = 1 by A15, A18, FINSEQ_1:39;

then Seg 1 = dom s by FINSEQ_1:def 3;

then A20: 1 in dom s by FINSEQ_1:2, TARSKI:def 1;

then consider b1, b2 being bag of {} such that

(decomp (EmptyBag {})) /. 1 = <*b1,b2*> and

A21: s /. 1 = (p . b1) * (q . b2) by A19;

s . 1 = (p . b1) * (q . b2) by A20, A21, PARTFUN1:def 6

.= (p . i) * (q . b2) by A3

.= (p . i) * (q . i) by A3 ;

then s = <*((p . i) * (q . i))*> by A16, A18, FINSEQ_1:40;

then Sum s = (p . i) * (q . i) by RLVECT_1:44;

hence (p *' q) . {} = (p . i) * (q . i) by A3, A17; :: thesis: verum

end;then A16: len (decomp (EmptyBag {})) = 1 by FINSEQ_1:39;

set z = (p . i) * (q . i);

consider s being FinSequence of the carrier of L such that

A17: (p *' q) . (EmptyBag {}) = Sum s and

A18: len s = len (decomp (EmptyBag {})) and

A19: for k being Element of NAT st k in dom s holds

ex b1, b2 being bag of {} st

( (decomp (EmptyBag {})) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by POLYNOM1:def 10;

len s = 1 by A15, A18, FINSEQ_1:39;

then Seg 1 = dom s by FINSEQ_1:def 3;

then A20: 1 in dom s by FINSEQ_1:2, TARSKI:def 1;

then consider b1, b2 being bag of {} such that

(decomp (EmptyBag {})) /. 1 = <*b1,b2*> and

A21: s /. 1 = (p . b1) * (q . b2) by A19;

s . 1 = (p . b1) * (q . b2) by A20, A21, PARTFUN1:def 6

.= (p . i) * (q . b2) by A3

.= (p . i) * (q . i) by A3 ;

then s = <*((p . i) * (q . i))*> by A16, A18, FINSEQ_1:40;

then Sum s = (p . i) * (q . i) by RLVECT_1:44;

hence (p *' q) . {} = (p . i) * (q . i) by A3, A17; :: thesis: verum

( pq = x * y & pq . {} = f . (x * y) ) by A7;

hence f . (x * y) = (f . x) * (f . y) by A12, A13, A14, POLYNOM1:def 11; :: thesis: verum

for x, y being Element of (Polynom-Ring ({},L)) holds f . (x + y) = (f . x) + (f . y)

proof

then A32:
f is additive
by VECTSP_1:def 20;
let x, y be Element of (Polynom-Ring ({},L)); :: thesis: f . (x + y) = (f . x) + (f . y)

consider p being Polynomial of {},L such that

A23: p = x and

A24: p . {} = f . x by A7;

consider q being Polynomial of {},L such that

A25: q = y and

A26: q . {} = f . y by A7;

consider a being Element of L such that

A27: p = {(EmptyBag {})} --> a by Lm1;

A28: ex pq being Polynomial of {},L st

( pq = x + y & pq . {} = f . (x + y) ) by A7;

consider b being Element of L such that

A29: q = {(EmptyBag {})} --> b by Lm1;

A30: p . {} = a by A4, A27;

A31: (p + q) . {} = (p . i) + (q . i) by POLYNOM1:15

.= a + b by A4, A30, A29 ;

q . {} = b by A4, A29;

then (f . x) + (f . y) = a + b by A4, A24, A26, A27;

hence f . (x + y) = (f . x) + (f . y) by A23, A25, A28, A31, POLYNOM1:def 11; :: thesis: verum

end;consider p being Polynomial of {},L such that

A23: p = x and

A24: p . {} = f . x by A7;

consider q being Polynomial of {},L such that

A25: q = y and

A26: q . {} = f . y by A7;

consider a being Element of L such that

A27: p = {(EmptyBag {})} --> a by Lm1;

A28: ex pq being Polynomial of {},L st

( pq = x + y & pq . {} = f . (x + y) ) by A7;

consider b being Element of L such that

A29: q = {(EmptyBag {})} --> b by Lm1;

A30: p . {} = a by A4, A27;

A31: (p + q) . {} = (p . i) + (q . i) by POLYNOM1:15

.= a + b by A4, A30, A29 ;

q . {} = b by A4, A29;

then (f . x) + (f . y) = a + b by A4, A24, A26, A27;

hence f . (x + y) = (f . x) + (f . y) by A23, A25, A28, A31, POLYNOM1:def 11; :: thesis: verum

p . i = p . (EmptyBag {}) by A3

.= ((0_ ({},L)) +* ((EmptyBag {}) .--> (1_ L))) . (EmptyBag {}) by A11, A1, FUNCT_7:def 3

.= ((EmptyBag {}) .--> (1_ L)) . (EmptyBag {}) by A2, FUNCT_4:13

.= 1_ L by FUNCOP_1:72 ;

then f is unity-preserving by A9, A10, GROUP_1:def 13;

then A33: f is RingHomomorphism by A32, A22;

A34: for u being object st u in the carrier of L holds

u in rng f

proof

rng f c= the carrier of L
by RELAT_1:def 19;
let u be object ; :: thesis: ( u in the carrier of L implies u in rng f )

assume u in the carrier of L ; :: thesis: u in rng f

then reconsider u = u as Element of L ;

set p = (EmptyBag {}) .--> u;

reconsider p = (EmptyBag {}) .--> u as Function ;

( rng p = {u} & dom p = Bags {} ) by FUNCOP_1:8, PRE_POLY:51, TARSKI:def 1;

then reconsider p = p as Function of (Bags {}), the carrier of L by FUNCT_2:2;

reconsider p = p as Function of (Bags {}),L ;

reconsider p = p as Series of {},L ;

reconsider p9 = p as Element of (Polynom-Ring ({},L)) by POLYNOM1:def 11;

consider q being Polynomial of {},L such that

A40: q = p9 and

A41: q . {} = f . p9 by A7;

q . {} = p . (EmptyBag {}) by A3, A40

.= u by FUNCOP_1:72 ;

hence u in rng f by A8, A41, FUNCT_1:3; :: thesis: verum

end;assume u in the carrier of L ; :: thesis: u in rng f

then reconsider u = u as Element of L ;

set p = (EmptyBag {}) .--> u;

reconsider p = (EmptyBag {}) .--> u as Function ;

( rng p = {u} & dom p = Bags {} ) by FUNCOP_1:8, PRE_POLY:51, TARSKI:def 1;

then reconsider p = p as Function of (Bags {}), the carrier of L by FUNCT_2:2;

reconsider p = p as Function of (Bags {}),L ;

reconsider p = p as Series of {},L ;

now :: thesis: ( ( u = 0. L & Support p is finite ) or ( u <> 0. L & Support p is finite ) )end;

then reconsider p = p as Polynomial of {},L by POLYNOM1:def 5;per cases
( u = 0. L or u <> 0. L )
;

end;

case A35:
u = 0. L
; :: thesis: Support p is finite

Support p = {}

end;proof

hence
Support p is finite
; :: thesis: verum
set v = the Element of Support p;

assume Support p <> {} ; :: thesis: contradiction

then A36: the Element of Support p in Support p ;

then the Element of Support p is bag of {} ;

then p . the Element of Support p = p . (EmptyBag {}) by A3, A4

.= u by FUNCOP_1:72 ;

hence contradiction by A35, A36, POLYNOM1:def 4; :: thesis: verum

end;assume Support p <> {} ; :: thesis: contradiction

then A36: the Element of Support p in Support p ;

then the Element of Support p is bag of {} ;

then p . the Element of Support p = p . (EmptyBag {}) by A3, A4

.= u by FUNCOP_1:72 ;

hence contradiction by A35, A36, POLYNOM1:def 4; :: thesis: verum

case A37:
u <> 0. L
; :: thesis: Support p is finite

A38:
for v being object st v in {(EmptyBag {})} holds

v in Support p

v in {(EmptyBag {})}

end;v in Support p

proof

for v being object st v in Support p holds
let v be object ; :: thesis: ( v in {(EmptyBag {})} implies v in Support p )

assume A39: v in {(EmptyBag {})} ; :: thesis: v in Support p

then reconsider v = v as Element of Bags {} ;

p . v = p . (EmptyBag {}) by A39, TARSKI:def 1

.= u by FUNCOP_1:72 ;

hence v in Support p by A37, POLYNOM1:def 4; :: thesis: verum

end;assume A39: v in {(EmptyBag {})} ; :: thesis: v in Support p

then reconsider v = v as Element of Bags {} ;

p . v = p . (EmptyBag {}) by A39, TARSKI:def 1

.= u by FUNCOP_1:72 ;

hence v in Support p by A37, POLYNOM1:def 4; :: thesis: verum

v in {(EmptyBag {})}

proof

hence
Support p is finite
by A38, TARSKI:2; :: thesis: verum
let v be object ; :: thesis: ( v in Support p implies v in {(EmptyBag {})} )

assume v in Support p ; :: thesis: v in {(EmptyBag {})}

then reconsider v = v as bag of {} ;

v = EmptyBag {} by A3, A4;

hence v in {(EmptyBag {})} by TARSKI:def 1; :: thesis: verum

end;assume v in Support p ; :: thesis: v in {(EmptyBag {})}

then reconsider v = v as bag of {} ;

v = EmptyBag {} by A3, A4;

hence v in {(EmptyBag {})} by TARSKI:def 1; :: thesis: verum

reconsider p9 = p as Element of (Polynom-Ring ({},L)) by POLYNOM1:def 11;

consider q being Polynomial of {},L such that

A40: q = p9 and

A41: q . {} = f . p9 by A7;

q . {} = p . (EmptyBag {}) by A3, A40

.= u by FUNCOP_1:72 ;

hence u in rng f by A8, A41, FUNCT_1:3; :: thesis: verum

then for u being object st u in rng f holds

u in the carrier of L ;

then rng f = the carrier of L by A34, TARSKI:2;

then f is onto ;

then A42: f is RingEpimorphism by A33;

for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds

x1 = x2

proof

then
f is one-to-one
by FUNCT_1:def 4;
let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )

assume that

A43: ( x1 in dom f & x2 in dom f ) and

A44: f . x1 = f . x2 ; :: thesis: x1 = x2

reconsider x1 = x1, x2 = x2 as Element of (Polynom-Ring ({},L)) by A43;

consider p being Polynomial of {},L such that

A45: ( p = x1 & p . {} = f . x1 ) by A7;

consider q being Polynomial of {},L such that

A46: ( q = x2 & q . {} = f . x2 ) by A7;

consider a2 being Element of L such that

A47: q = {(EmptyBag {})} --> a2 by Lm1;

A48: q . (EmptyBag {}) = a2 by A47;

A49: p . {} = p . (EmptyBag {}) by A3;

consider a1 being Element of L such that

A50: p = {(EmptyBag {})} --> a1 by Lm1;

thus x1 = x2 by A3, A44, A45, A46, A50, A47, A48, A49; :: thesis: verum

end;assume that

A43: ( x1 in dom f & x2 in dom f ) and

A44: f . x1 = f . x2 ; :: thesis: x1 = x2

reconsider x1 = x1, x2 = x2 as Element of (Polynom-Ring ({},L)) by A43;

consider p being Polynomial of {},L such that

A45: ( p = x1 & p . {} = f . x1 ) by A7;

consider q being Polynomial of {},L such that

A46: ( q = x2 & q . {} = f . x2 ) by A7;

consider a2 being Element of L such that

A47: q = {(EmptyBag {})} --> a2 by Lm1;

A48: q . (EmptyBag {}) = a2 by A47;

A49: p . {} = p . (EmptyBag {}) by A3;

consider a1 being Element of L such that

A50: p = {(EmptyBag {})} --> a1 by Lm1;

thus x1 = x2 by A3, A44, A45, A46, A50, A47, A48, A49; :: thesis: verum

then f is RingMonomorphism by A33;

then f is RingIsomorphism by A42;

hence Polynom-Ring ({},L) is_ringisomorph_to L by QUOFIELD:def 23; :: thesis: verum