deffunc H₁( set ) -> Element of bool [:(Bags {}),{$1}:] = (Bags {}) --> $1;
let R be non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; :: thesis:
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 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 4;
then y9 in the carrier of (Polynom-Ring (0,R)) by POLYNOM1:def 10;
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 10;
A5: dom y9 = Bags {} by FUNCT_2:def 1;
then A6: 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 . {}) by A5, A6, FUNCOP_1:9;
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:1;
then reconsider P = P as Function of R,(Polynom-Ring (0,R)) by A1, FUNCT_2:1;
A8: EmptyBag {} = {} --> 0 by PRE_POLY: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 10;

now

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

end;

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

end;

then A12: P is additive by GRCAT_1:def 8;

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

now

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

now

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

end;

then A23: P is multiplicative by GROUP_6:def 6;
take P ; :: thesis:
reconsider f0 = {{}} --> (0. R), f1 = {{}} --> (1_ R) as Function of {{}}, the carrier of R ;
A24: dom f1 = {{}} by FUNCT_2:def 1;
A25: dom f0 = {{}} by FUNCT_2:def 1;
then A26: {} 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 A8, POLYNOM1:def 8
.= ({{}} --> (0. R)) +* ({},(1_ R)) by POLYNOM1:def 7, PRE_POLY:51
.= ({{}} --> (0. R)) +* ({} .--> (1_ R)) by A26, FUNCT_7:def 3
.= {{}} --> (1_ R) by A25, A24, FUNCT_4:19
.= P . (1_ R) by A2, PRE_POLY:51 ;
then P is unity-preserving by GROUP_1:def 13;
then A27: P is RingHomomorphism by A12, A23, QUOFIELD:def 18;
then A28: P is RingEpimorphism by A7, QUOFIELD:def 19;

now

let x1, x2 be set ; :: thesis:
assume that
A29: x1 in dom P and
A30: x2 in dom P ; :: thesis:
assume P . x1 = P . x2 ; :: thesis:
then (Bags {}) --> x1 = P . x2 by A2, A29;
then (Bags {}) --> x1 = (Bags {}) --> x2 by A2, A30;
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 A27, QUOFIELD:def 20;
hence P is RingIsomorphism by A28, QUOFIELD:def 21; :: thesis: