set n = {} ;
let L be non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; :: thesis:
set PL = Polynom-Ring {} ,L;
defpred S₁[ set , set ] means ex p being Polynomial of {} ,L st
( p = $1 & p . {} = $2 );
A1: dom (0_ {} ,L) = Bags {} by FUNCT_2:def 1;
dom ((EmptyBag {} ) .--> (1_ L)) = {(EmptyBag {} )} by FUNCOP_1:19;
then A2: EmptyBag {} in dom ((EmptyBag {} ) .--> (1_ L)) by TARSKI:def 1;
A3: for b being bag of {} holds b = {}

proof

let b be bag of {} ; :: thesis:
b in Bags {} by PRE_POLY:def 12;
hence b = {} by PRE_POLY:51, TARSKI:def 1; :: thesis:

end;

then A4: EmptyBag {} = {} ;
then reconsider i = {} as bag of {} ;
A5: 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 A6: p . {} in rng p by A4, 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 A6; :: thesis:

end;

consider f being Function of the carrier of (Polynom-Ring {} ,L),the carrier of L such that
A7: for x being Element of (Polynom-Ring {} ,L) holds S₁[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:90
.= (0_ {} ,L) +* (EmptyBag {} ),(1_ L) by POLYNOM1:def 25 ;
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
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

A15: decomp (EmptyBag {} ) = <*<*(EmptyBag {} ),(EmptyBag {} )*>*> by PRE_POLY:73;
then A16: len (decomp (EmptyBag {} )) = 1 by FINSEQ_1:56;
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 26;
len s = 1 by A15, A18, FINSEQ_1:56;
then Seg 1 = dom s by FINSEQ_1:def 3;
then A20: 1 in dom s by FINSEQ_1:4, 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 8
.= (p . i) * (q . b2) by A3
.= (p . i) * (q . i) by A3 ;
then s = <*((p . i) * (q . i))*> by A16, A18, FINSEQ_1:57;
then Sum s = (p . i) * (q . i) by RLVECT_1:61;
hence (p *' q) . {} = (p . i) * (q . i) by A3, A17; :: thesis:

end;

ex pq being Polynomial of {} ,L st
( pq = x * y & pq . {} = f . (x * y) ) by A7;
hence f . (x * y) = (f . x) * (f . y) by A12, A13, A14, POLYNOM1:def 27; :: thesis:

end;

then A22: f is multiplicative by GROUP_6:def 7;
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
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: EmptyBag {} in {(EmptyBag {} )} by TARSKI:def 1;
then A31: p . {} = a by A4, A27, FUNCOP_1:13;
A32: (p + q) . {} = (p . i) + (q . i) by POLYNOM1:def 21
.= a + b by A4, A30, A31, A29, FUNCOP_1:13 ;
q . {} = b by A4, A30, A29, FUNCOP_1:13;
then (f . x) + (f . y) = a + b by A4, A24, A26, A27, A30, FUNCOP_1:13;
hence f . (x + y) = (f . x) + (f . y) by A23, A25, A28, A32, POLYNOM1:def 27; :: thesis:

end;

then A33: f is additive by GRCAT_1:def 13;
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:14
.= 1_ L by FUNCOP_1:87 ;
then f is unity-preserving by A9, A10, GROUP_1:def 17;
then A34: f is RingHomomorphism by A33, A22, QUOFIELD:def 21;
A35: 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 {} )} by FUNCOP_1:19;
then ( rng p = {u} & dom p = Bags {} ) by FUNCOP_1:14, PRE_POLY:51, 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 A36: u = 0. L ; :: thesis:

Support p = {}

proof

consider v being Element of Support p;
assume Support p <> {} ; :: thesis:
then A37: v in Support p ;
then v is bag of {} ;
then p . v = p . (EmptyBag {} ) by A3, A4
.= u by FUNCOP_1:87 ;
hence contradiction by A36, A37, POLYNOM1:def 9; :: thesis:

end;

hence Support p is finite ; :: thesis:

end;

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

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

proof

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

end;

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 {} ;
v = EmptyBag {} by A3, A4;
hence v in {(EmptyBag {} )} by TARSKI:def 1; :: thesis:

end;

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

end;

then reconsider p = p as Polynomial of {} ,L by POLYNOM1:def 10;
reconsider p9 = p as Element of (Polynom-Ring {} ,L) by POLYNOM1:def 27;
consider q being Polynomial of {} ,L such that
A41: q = p9 and
A42: q . {} = f . p9 by A7;
q . {} = p . (EmptyBag {} ) by A3, A41
.= u by FUNCOP_1:87 ;
hence u in rng f by A8, A42, FUNCT_1:12; :: thesis:

end;

rng f c= the carrier of L by RELAT_1:def 19;
then for u being set st u in rng f holds
u in the carrier of L ;
then rng f = the carrier of L by A35, TARSKI:2;
then A43: f is RingEpimorphism by A34, QUOFIELD:def 22;
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 that
A44: ( x1 in dom f & x2 in dom f ) and
A45: f . x1 = f . x2 ; :: thesis:
reconsider x1 = x1, x2 = x2 as Element of (Polynom-Ring {} ,L) by A44;
consider p being Polynomial of {} ,L such that
A46: ( p = x1 & p . {} = f . x1 ) by A7;
consider q being Polynomial of {} ,L such that
A47: ( q = x2 & q . {} = f . x2 ) by A7;
consider a2 being Element of L such that
A48: q = {(EmptyBag {} )} --> a2 by Lm1;
A49: EmptyBag {} in {(EmptyBag {} )} by TARSKI:def 1;
then A50: q . (EmptyBag {} ) = a2 by A48, FUNCOP_1:13;
A51: p . {} = p . (EmptyBag {} ) by A3;
consider a1 being Element of L such that
A52: p = {(EmptyBag {} )} --> a1 by Lm1;
p . (EmptyBag {} ) = a1 by A52, A49, FUNCOP_1:13;
hence x1 = x2 by A3, A45, A46, A47, A52, A48, A50, A51; :: thesis:

end;

then f is one-to-one by FUNCT_1:def 8;
then f is RingMonomorphism by A34, QUOFIELD:def 23;
then f is RingIsomorphism by A43, QUOFIELD:def 24;
hence Polynom-Ring {} ,L is_ringisomorph_to L by QUOFIELD:def 26; :: thesis: