let R be non empty non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; :: thesis:
deffunc H₁( set ) -> Element of bool [:(Bags {} ),{$1}:] = (Bags {} ) --> $1;
consider P being Function such that
A1: dom P = the carrier of R and
A2: for x being set st x in the carrier of R holds
P . x = H₁(x) from FUNCT_1:sch 3();

now

let y be set ; :: thesis:

hereby :: thesis:

assume y in rng P ; :: thesis:
then consider x being set such that
A3: ( x in the carrier of R & y = P . x ) by A1, FUNCT_1:def 5;
reconsider x = x as Element of R by A3;
reconsider y' = (Bags {} ) --> x as Function of (Bags {} ),R ;
Support y' is finite by POLYNOM1:55;
then y' is finite-Support Series of 0 ,R by POLYNOM1:def 10;
then y' in the carrier of (Polynom-Ring 0 ,R) by POLYNOM1:def 27;
hence y in the carrier of (Polynom-Ring 0 ,R) by A2, A3; :: thesis:

end;

assume y in the carrier of (Polynom-Ring 0 ,R) ; :: thesis:
then reconsider y' = y as Function of (Bags {} ),R by POLYNOM1:def 27;
A4: dom y' = Bags {} by FUNCT_2:def 1;
then A5: rng y' = {(y' . {} )} by FUNCT_1:14, POLYNOM1:55;
then A6: y' = (Bags {} ) --> (y' . {} ) by A4, FUNCOP_1:15;
y' . {} in rng y' by A5, TARSKI:def 1;
then reconsider x = y' . {} as Element of R ;
y = P . x by A2, A6;
hence y in rng P by A1, FUNCT_1:def 5; :: thesis:

end;

then A7: rng P = the carrier of (Polynom-Ring 0 ,R) by TARSKI:2;
then reconsider P = P as Function of R,(Polynom-Ring 0 ,R) by A1, FUNCT_2:3;
take P ; :: thesis:

now

let x, y be Element of R; :: thesis:
reconsider Px = P . x, Py = P . y, Pxy = P . (x + y) as Polynomial of 0 ,R by POLYNOM1:def 27;

now

let z be bag of ; :: thesis:
A8: z in Bags {} by POLYNOM1:def 14;
A9: Pxy . z = ((Bags {} ) --> (x + y)) . z by A2
.= x + y by A8, FUNCOP_1:13 ;
A10: Px . z = ((Bags {} ) --> x) . z by A2
.= x by A8, FUNCOP_1:13 ;
Py . z = ((Bags {} ) --> y) . z by A2
.= y by A8, FUNCOP_1:13 ;
hence Pxy . z = (Px . z) + (Py . z) by A9, A10; :: thesis:

end;

then Pxy = Px + Py by POLYNOM1:def 21;
hence (P . x) + (P . y) = P . (x + y) by POLYNOM1:def 27; :: thesis:

end;

then A11: P is additive by GRCAT_1:def 13;

now

let x, y be Element of R; :: thesis:
reconsider Px = P . x, Py = P . y, Pxy = P . (x * y) as Polynomial of 0 ,R by POLYNOM1:def 27;

now

let b be bag of ; :: thesis:
reconsider s = <*(x * y)*> as FinSequence of the carrier of R ;
take s = s; :: thesis:
A12: b in Bags {} by POLYNOM1:def 14;
thus Pxy . b = ((Bags {} ) --> (x * y)) . b by A2
.= x * y by A12, FUNCOP_1:13
.= Sum s by RLVECT_1:61 ; :: thesis:
A13: decomp b = <*<*{} ,{} *>*> by Th2;
A14: len s = 1 by FINSEQ_1:56;
A15: len (decomp b) = 1 by A13, FINSEQ_1:56;
thus len s = len (decomp b) by A13, A14, FINSEQ_1:56; :: thesis:

now

let k be Element of NAT ; :: thesis:
assume A16: k in dom s ; :: thesis:
then A17: ( 1 <= k & k <= 1 ) by A14, FINSEQ_3:27;
then A18: k = 1 by XXREAL_0:1;
set b1 = {} ;
set b2 = {} ;
A19: ( {} in Bags {} & {} in Bags {} ) by POLYNOM1:55, TARSKI:def 1;
then reconsider b1 = {} , b2 = {} as bag of by POLYNOM1:def 14;
take b1 = b1; :: thesis:
take b2 = b2; :: thesis:
k in dom (decomp b) by A15, A17, FINSEQ_3:27;
hence (decomp b) /. k = (decomp b) . 1 by A18, PARTFUN1:def 8
.= <*b1,b2*> by A13, FINSEQ_1:57 ;
:: thesis:
A20: Px . b1 = ((Bags {} ) --> x) . b1 by A2
.= x by A19, FUNCOP_1:13 ;
A21: Py . b2 = ((Bags {} ) --> y) . b2 by A2
.= y by A19, FUNCOP_1:13 ;
thus s /. k = s . 1 by A16, A18, PARTFUN1:def 8
.= (Px . b1) * (Py . b2) by A20, A21, FINSEQ_1:57 ; :: thesis:

end;

hence for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of st
( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) ; :: thesis:

end;

then Pxy = Px *' Py by POLYNOM1:def 26;
hence (P . x) * (P . y) = P . (x * y) by POLYNOM1:def 27; :: thesis:

end;

then A22: P is multiplicative by GROUP_6:def 7;
A23: EmptyBag {} = {} --> 0 by POLYNOM1:def 15;
reconsider f0 = {{} } --> (0. R), f1 = {{} } --> (1_ R) as Function of {{} },the carrier of R ;
A24: dom f0 = {{} } by FUNCT_2:def 1;
then A25: {} in dom ({{} } --> (0. R)) by TARSKI:def 1;
A26: dom f1 = {{} } by FUNCT_2:def 1;
1_ (Polynom-Ring 0 ,R) = 1_ 0 ,R by POLYNOM1:90
.= (0_ 0 ,R) +* {} ,(1_ R) by A23, POLYNOM1:def 25
.= ({{} } --> (0. R)) +* {} ,(1_ R) by POLYNOM1:55, POLYNOM1:def 24
.= ({{} } --> (0. R)) +* ({} .--> (1_ R)) by A25, FUNCT_7:def 3
.= {{} } --> (1_ R) by A24, A26, FUNCT_4:20
.= P . (1_ R) by A2, POLYNOM1:55 ;
then P is unity-preserving by GROUP_1:def 17;
then A27: P is RingHomomorphism by A11, A22, QUOFIELD:def 21;

now

let x1, x2 be set ; :: thesis:
assume A28: ( x1 in dom P & x2 in dom P ) ; :: thesis:
assume P . x1 = P . x2 ; :: thesis:
then (Bags {} ) --> x1 = P . x2 by A2, A28;
then (Bags {} ) --> x1 = (Bags {} ) --> x2 by A2, A28;
hence x1 = x2 by FUNCT_4:7; :: thesis:

end;

then P is one-to-one by FUNCT_1:def 8;
then A29: P is RingMonomorphism by A27, QUOFIELD:def 23;
P is RingEpimorphism by A7, A27, QUOFIELD:def 22;
hence P is RingIsomorphism by A29, QUOFIELD:def 24; :: thesis: