let L be non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; :: thesis:
set n = {} ;
set PL = Polynom-Ring {} ,L;
A1: for b being bag of holds b = {}

proof

let b be bag of ; :: thesis:
b in Bags {} by POLYNOM1:def 14;
hence b = {} by POLYNOM1:55, TARSKI:def 1; :: thesis:

end;

then A2: EmptyBag {} = {} ;
then reconsider i = {} as bag of ;
defpred S₁[ set , set ] means ex p being Polynomial of {} ,L st
( p = $1 & p . {} = $2 );
A3: for x being Element of (Polynom-Ring {} ,L) ex y being Element of L st S₁[x,y]

proof

let x be Element of (Polynom-Ring {} ,L); :: thesis:
reconsider p = x as Polynomial of {} ,L by POLYNOM1:def 27;
take p . {} ; :: thesis:
dom p = Bags {} by FUNCT_2:def 1;
then A4: p . {} in rng p by A2, FUNCT_1:12;
rng p c= the carrier of L by RELAT_1:def 19;
hence ( p . {} is Element of L & S₁[x,p . {} ] ) by A4; :: thesis:

end;

consider f being Function of the carrier of (Polynom-Ring {} ,L),the carrier of L such that
A5: for x being Element of (Polynom-Ring {} ,L) holds S₁[x,f . x] from FUNCT_2:sch 3(A3);
A6: dom f = the carrier of (Polynom-Ring {} ,L) by FUNCT_2:def 1;
reconsider f = f as Function of (Polynom-Ring {} ,L),L ;
for x, y being Element of (Polynom-Ring {} ,L) holds f . (x + y) = (f . x) + (f . y)

proof

let x, y be Element of (Polynom-Ring {} ,L); :: thesis:
consider p being Polynomial of {} ,L such that
A7: ( p = x & p . {} = f . x ) by A5;
consider q being Polynomial of {} ,L such that
A8: ( q = y & q . {} = f . y ) by A5;
consider a being Element of L such that
A9: p = {(EmptyBag {} )} --> a by Lm1;
A10: EmptyBag {} in {(EmptyBag {} )} by TARSKI:def 1;
then A11: p . {} = a by A2, A9, FUNCOP_1:13;
consider b being Element of L such that
A12: q = {(EmptyBag {} )} --> b by Lm1;
q . {} = b by A2, A10, A12, FUNCOP_1:13;
then A13: (f . x) + (f . y) = a + b by A2, A7, A8, A9, A10, FUNCOP_1:13;
consider pq being Polynomial of {} ,L such that
A14: ( pq = x + y & pq . {} = f . (x + y) ) by A5;
(p + q) . {} = (p . i) + (q . i) by POLYNOM1:def 21
.= a + b by A2, A10, A11, A12, FUNCOP_1:13 ;
hence f . (x + y) = (f . x) + (f . y) by A7, A8, A13, A14, POLYNOM1:def 27; :: thesis:

end;

then A15: f is additive by GRCAT_1:def 13;
for x, y being Element of (Polynom-Ring {} ,L) holds f . (x * y) = (f . x) * (f . y)

proof

let x, y be Element of (Polynom-Ring {} ,L); :: thesis:
consider p being Polynomial of {} ,L such that
A16: ( p = x & p . {} = f . x ) by A5;
consider q being Polynomial of {} ,L such that
A17: ( q = y & q . {} = f . y ) by A5;
consider pq being Polynomial of {} ,L such that
A18: ( pq = x * y & pq . {} = f . (x * y) ) by A5;
(p *' q) . {} = (p . i) * (q . i)

proof

set z = (p . i) * (q . i);
A19: decomp (EmptyBag {} ) = <*<*(EmptyBag {} ),(EmptyBag {} )*>*> by POLYNOM1:77;
then A20: len (decomp (EmptyBag {} )) = 1 by FINSEQ_1:56;
consider s being FinSequence of the carrier of L such that
A21: ( (p *' q) . (EmptyBag {} ) = Sum s & len s = len (decomp (EmptyBag {} )) & ( 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 26;
len s = 1 by A19, A21, FINSEQ_1:56;
then Seg 1 = dom s by FINSEQ_1:def 3;
then A22: 1 in dom s by FINSEQ_1:4, TARSKI:def 1;
then consider b1, b2 being bag of such that
A23: ( (decomp (EmptyBag {} )) /. 1 = <*b1,b2*> & s /. 1 = (p . b1) * (q . b2) ) by A21;
s . 1 = (p . b1) * (q . b2) by A22, A23, PARTFUN1:def 8
.= (p . i) * (q . b2) by A1
.= (p . i) * (q . i) by A1 ;
then s = <*((p . i) * (q . i))*> by A20, A21, FINSEQ_1:57;
then Sum s = (p . i) * (q . i) by RLVECT_1:61;
hence (p *' q) . {} = (p . i) * (q . i) by A1, A21; :: thesis:

end;

hence f . (x * y) = (f . x) * (f . y) by A16, A17, A18, POLYNOM1:def 27; :: thesis:

end;

then A24: f is multiplicative by GROUP_6:def 7;
consider p being Polynomial of {} ,L such that
A25: ( p = 1_ (Polynom-Ring {} ,L) & p . {} = f . (1. (Polynom-Ring {} ,L)) ) by A5;
A26: p = 1_ {} ,L by A25, POLYNOM1:90
.= (0_ {} ,L) +* (EmptyBag {} ),(1_ L) by POLYNOM1:def 25 ;
A27: dom (0_ {} ,L) = Bags {} by FUNCT_2:def 1;
dom ((EmptyBag {} ) .--> (1_ L)) = {(EmptyBag {} )} by FUNCOP_1:19;
then A28: EmptyBag {} in dom ((EmptyBag {} ) .--> (1_ L)) by TARSKI:def 1;
p . i = p . (EmptyBag {} ) by A1
.= ((0_ {} ,L) +* ((EmptyBag {} ) .--> (1_ L))) . (EmptyBag {} ) by A26, A27, FUNCT_7:def 3
.= ((EmptyBag {} ) .--> (1_ L)) . (EmptyBag {} ) by A28, FUNCT_4:14
.= 1_ L by FUNCOP_1:87 ;
then f is unity-preserving by A25, GROUP_1:def 17;
then A29: f is RingHomomorphism by A15, A24, QUOFIELD:def 21;
for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis:
assume A30: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis:
then reconsider x1 = x1, x2 = x2 as Element of (Polynom-Ring {} ,L) ;
consider p being Polynomial of {} ,L such that
A31: ( p = x1 & p . {} = f . x1 ) by A5;
consider q being Polynomial of {} ,L such that
A32: ( q = x2 & q . {} = f . x2 ) by A5;
consider a1 being Element of L such that
A33: p = {(EmptyBag {} )} --> a1 by Lm1;
consider a2 being Element of L such that
A34: q = {(EmptyBag {} )} --> a2 by Lm1;
EmptyBag {} in {(EmptyBag {} )} by TARSKI:def 1;
then A35: ( p . (EmptyBag {} ) = a1 & q . (EmptyBag {} ) = a2 ) by A33, A34, FUNCOP_1:13;
( p . {} = p . (EmptyBag {} ) & q . {} = q . (EmptyBag {} ) ) by A1;
hence x1 = x2 by A30, A31, A32, A33, A34, A35; :: thesis:

end;

then f is one-to-one by FUNCT_1:def 8;
then A36: f is RingMonomorphism by A29, QUOFIELD:def 23;
rng f c= the carrier of L by RELAT_1:def 19;
then A37: for u being set st u in rng f holds
u in the carrier of L ;
for u being set st u in the carrier of L holds
u in rng f

proof

let u be set ; :: thesis:
assume u in the carrier of L ; :: thesis:
then reconsider u = u as Element of L ;
set p = (EmptyBag {} ) .--> u;
reconsider p = (EmptyBag {} ) .--> u as Function ;
( dom p = {(EmptyBag {} )} & rng p = {u} ) by FUNCOP_1:14, FUNCOP_1:19;
then ( dom p = Bags {} & rng p c= the carrier of L ) by POLYNOM1:55, TARSKI:def 1;
then reconsider p = p as Function of (Bags {} ),the carrier of L by FUNCT_2:4;
reconsider p = p as Function of (Bags {} ),L ;
reconsider p = p as Series of {} ,L ;

now

per cases ;

case A38: u = 0. L ; :: thesis:

Support p = {}

proof

assume A39: Support p <> {} ; :: thesis:
consider v being Element of Support p;
A40: v in Support p by A39;
then v is bag of by POLYNOM1:def 14;
then p . v = p . (EmptyBag {} ) by A1, A2
.= u by FUNCOP_1:87 ;
hence contradiction by A38, A40, POLYNOM1:def 9; :: thesis:

end;

hence Support p is finite ; :: thesis:

end;

case A41: u <> 0. L ; :: thesis:

A42: for v being set st v in Support p holds
v in {(EmptyBag {} )}

proof

let v be set ; :: thesis:
assume v in Support p ; :: thesis:
then reconsider v = v as bag of by POLYNOM1:def 14;
v = EmptyBag {} by A1, A2;
hence v in {(EmptyBag {} )} by TARSKI:def 1; :: thesis:

end;

for v being set st v in {(EmptyBag {} )} holds
v in Support p

proof

let v be set ; :: thesis:
assume A43: v in {(EmptyBag {} )} ; :: thesis:
then reconsider v = v as Element of Bags {} ;
p . v = p . (EmptyBag {} ) by A43, TARSKI:def 1
.= u by FUNCOP_1:87 ;
hence v in Support p by A41, POLYNOM1:def 9; :: thesis:

end;

hence Support p is finite by A42, TARSKI:2; :: thesis:

end;

then reconsider p = p as Polynomial of {} ,L by POLYNOM1:def 10;
reconsider p' = p as Element of (Polynom-Ring {} ,L) by POLYNOM1:def 27;
consider q being Polynomial of {} ,L such that
A44: ( q = p' & q . {} = f . p' ) by A5;
q . {} = p . (EmptyBag {} ) by A1, A44
.= u by FUNCOP_1:87 ;
hence u in rng f by A6, A44, FUNCT_1:12; :: thesis:

end;

then rng f = the carrier of L by A37, TARSKI:2;
then f is RingEpimorphism by A29, QUOFIELD:def 22;
then f is RingIsomorphism by A36, QUOFIELD:def 24;
hence Polynom-Ring {} ,L is_ringisomorph_to L by QUOFIELD:def 26; :: thesis: