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

now :: thesis:

let y be object ; :: thesis:

hereby :: thesis:

assume y in rng P ; :: thesis:
then consider x being object such that
A3: x in the carrier of R and
A4: y = P . x by A1, FUNCT_1:def 3;
reconsider x = x as Element of R by A3;
reconsider y9 = (Bags {}) --> x as Function of (Bags {}),R ;
Support y9 is finite by PRE_POLY:51;
then y9 is finite-Support Series of 0,R by POLYNOM1:def 5;
then y9 in the carrier of (Polynom-Ring (0,R)) by POLYNOM1:def 11;
hence y in the carrier of (Polynom-Ring (0,R)) by A2, A4; :: thesis:

end;

assume y in the carrier of (Polynom-Ring (0,R)) ; :: thesis:
then reconsider y9 = y as Function of (Bags {}),R by POLYNOM1:def 11;
dom y9 = Bags {} by FUNCT_2:def 1;
then rng y9 = {(y9 . {})} by FUNCT_1:4, PRE_POLY:51;
then y9 . {} in rng y9 by TARSKI:def 1;
then reconsider x = y9 . {} as Element of R ;
y9 = (Bags {}) --> (y9 . {}) ;
then y = P . x by A2;
hence y in rng P by A1, FUNCT_1:def 3; :: 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:1;
A8: P is onto by A7;
A9: EmptyBag {} = {} --> 0 ;

now :: thesis:

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 11;

now :: thesis:

let z be bag of 0 ; :: thesis:
A10: z in Bags {} by PRE_POLY:def 12;
A11: Py . z = ((Bags {}) --> y) . z by A2
.= y by A10, FUNCOP_1:7 ;
A12: Px . z = ((Bags {}) --> x) . z by A2
.= x by A10, FUNCOP_1:7 ;
Pxy . z = ((Bags {}) --> (x + y)) . z by A2
.= x + y by A10, FUNCOP_1:7 ;
hence Pxy . z = (Px . z) + (Py . z) by A12, A11; :: thesis:

end;

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

end;

then A13: P is additive ;

now :: thesis:

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 11;

now :: thesis:

reconsider s = <*(x * y)*> as FinSequence of the carrier of R ;
let b be bag of 0 ; :: thesis:
take s = s; :: thesis:
A14: b in Bags {} by PRE_POLY:def 12;
thus Pxy . b = ((Bags {}) --> (x * y)) . b by A2
.= x * y by A14, FUNCOP_1:7
.= Sum s by RLVECT_1:44 ; :: thesis:
A15: decomp b = <*<*{},{}*>*> by Th2;
A16: len s = 1 by FINSEQ_1:39;
hence len s = len (decomp b) by A15, FINSEQ_1:39; :: thesis:
A17: len (decomp b) = 1 by A15, FINSEQ_1:39;

now :: thesis:

set b1 = {} ;
set b2 = {} ;
let k be Element of NAT ; :: thesis:
A18: {} in Bags {} by PRE_POLY:51, TARSKI:def 1;
then reconsider b1 = {} , b2 = {} as bag of 0 ;
A19: Px . b1 = ((Bags {}) --> x) . b1 by A2
.= x by A18, FUNCOP_1:7 ;
A20: Py . b2 = ((Bags {}) --> y) . b2 by A2
.= y by A18, FUNCOP_1:7 ;
assume A21: k in dom s ; :: thesis:
then A22: ( 1 <= k & k <= 1 ) by A16, FINSEQ_3:25;
then A23: k = 1 by XXREAL_0:1;
take b1 = b1; :: thesis:
take b2 = b2; :: thesis:
k in dom (decomp b) by A17, A22, FINSEQ_3:25;
hence (decomp b) /. k = (decomp b) . 1 by A23, PARTFUN1:def 6
.= <*b1,b2*> by A15, FINSEQ_1:40 ;
:: thesis:
thus s /. k = s . 1 by A21, A23, PARTFUN1:def 6
.= (Px . b1) * (Py . b2) by A19, A20, FINSEQ_1:40 ; :: thesis:

end;

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

end;

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

end;

then A24: P is multiplicative ;
take P ; :: thesis:
reconsider f0 = {{}} --> (0. R), f1 = {{}} --> (1_ R) as Function of {{}}, the carrier of R ;
A25: dom f1 = {{}} ;
A26: dom f0 = {{}} ;
A27: {} in dom ({{}} --> (0. R)) by TARSKI:def 1;
1_ (Polynom-Ring (0,R)) = 1_ (0,R) by POLYNOM1:31
.= (0_ (0,R)) +* ({},(1_ R)) by A9, POLYNOM1:def 9
.= ({{}} --> (0. R)) +* ({},(1_ R)) by POLYNOM1:def 8, PRE_POLY:51
.= ({{}} --> (0. R)) +* ({} .--> (1_ R)) by A27, FUNCT_7:def 3
.= {{}} --> (1_ R) by A26, A25, FUNCT_4:19
.= P . (1_ R) by A2, PRE_POLY:51 ;
then P is unity-preserving by GROUP_1:def 13;
then A28: P is RingHomomorphism by A13, A24;
then A29: P is RingEpimorphism by A8;

now :: thesis:

let x1, x2 be object ; :: thesis:
assume that
A30: x1 in dom P and
A31: x2 in dom P ; :: thesis:
assume P . x1 = P . x2 ; :: thesis:
then (Bags {}) --> x1 = P . x2 by A2, A30;
then (Bags {}) --> x1 = (Bags {}) --> x2 by A2, A31;
hence x1 = x2 by FUNCT_4:6; :: thesis:

end;

then P is one-to-one by FUNCT_1:def 4;
then P is RingMonomorphism by A28;
hence P is RingIsomorphism by A29; :: thesis: