deffunc H_{1}( 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: ex P being Function of R,(Polynom-Ring (0,R)) st P is RingIsomorphism

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_{1}(x)
from FUNCT_1:sch 3();

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 ;

take P ; :: thesis: P is RingIsomorphism

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;

then P is RingMonomorphism by A28;

hence P is RingIsomorphism by A29; :: thesis: verum

let R be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: ex P being Function of R,(Polynom-Ring (0,R)) st P is RingIsomorphism

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

now :: thesis: for y being object holds

( ( y in rng P implies y in the carrier of (Polynom-Ring (0,R)) ) & ( y in the carrier of (Polynom-Ring (0,R)) implies y in rng P ) )

then A7:
rng P = the carrier of (Polynom-Ring (0,R))
by TARSKI:2;( ( y in rng P implies y in the carrier of (Polynom-Ring (0,R)) ) & ( y in the carrier of (Polynom-Ring (0,R)) implies y in rng P ) )

let y be object ; :: thesis: ( ( y in rng P implies y in the carrier of (Polynom-Ring (0,R)) ) & ( y in the carrier of (Polynom-Ring (0,R)) implies y in rng P ) )

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: verum

end;hereby :: thesis: ( y in the carrier of (Polynom-Ring (0,R)) implies y in rng P )

assume
y in the carrier of (Polynom-Ring (0,R))
; :: thesis: y in rng Passume
y in rng P
; :: thesis: y in the carrier of (Polynom-Ring (0,R))

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: verum

end;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: verum

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: verum

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: for x, y being Element of R holds (P . x) + (P . y) = P . (x + y)

then A13:
P is additive
;let x, y be Element of R; :: thesis: (P . x) + (P . y) = P . (x + y)

reconsider Px = P . x, Py = P . y, Pxy = P . (x + y) as Polynomial of 0,R by POLYNOM1:def 11;

hence (P . x) + (P . y) = P . (x + y) by POLYNOM1:def 11; :: thesis: verum

end;reconsider Px = P . x, Py = P . y, Pxy = P . (x + y) as Polynomial of 0,R by POLYNOM1:def 11;

now :: thesis: for z being bag of 0 holds Pxy . z = (Px . z) + (Py . z)

then
Pxy = Px + Py
by POLYNOM1:16;let z be bag of 0 ; :: thesis: Pxy . z = (Px . z) + (Py . z)

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: verum

end;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: verum

hence (P . x) + (P . y) = P . (x + y) by POLYNOM1:def 11; :: thesis: verum

now :: thesis: for x, y being Element of R holds (P . x) * (P . y) = P . (x * y)

then A24:
P is multiplicative
;let x, y be Element of R; :: thesis: (P . x) * (P . y) = P . (x * y)

reconsider Px = P . x, Py = P . y, Pxy = P . (x * y) as Polynomial of 0,R by POLYNOM1:def 11;

hence (P . x) * (P . y) = P . (x * y) by POLYNOM1:def 11; :: thesis: verum

end;reconsider Px = P . x, Py = P . y, Pxy = P . (x * y) as Polynomial of 0,R by POLYNOM1:def 11;

now :: thesis: for b being bag of 0 ex s being FinSequence of the carrier of R st

( Pxy . b = Sum s & len s = len (decomp b) & ( 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) ) ) )

then
Pxy = Px *' Py
by POLYNOM1:def 10;( Pxy . b = Sum s & len s = len (decomp b) & ( 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) ) ) )

reconsider s = <*(x * y)*> as FinSequence of the carrier of R ;

let b be bag of 0 ; :: thesis: ex s being FinSequence of the carrier of R st

( Pxy . b = Sum s & len s = len (decomp b) & ( 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) ) ) )

take s = s; :: thesis: ( Pxy . b = Sum s & len s = len (decomp b) & ( 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) ) ) )

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: ( len s = len (decomp b) & ( 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) ) ) )

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: 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) )

A17: len (decomp b) = 1 by A15, FINSEQ_1:39;

ex b1, b2 being bag of 0 st

( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) ; :: thesis: verum

end;let b be bag of 0 ; :: thesis: ex s being FinSequence of the carrier of R st

( Pxy . b = Sum s & len s = len (decomp b) & ( 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) ) ) )

take s = s; :: thesis: ( Pxy . b = Sum s & len s = len (decomp b) & ( 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) ) ) )

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: ( len s = len (decomp b) & ( 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) ) ) )

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: 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) )

A17: len (decomp b) = 1 by A15, FINSEQ_1:39;

now :: thesis: 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) )

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) )

set b1 = {} ;

set b2 = {} ;

let k be Element of NAT ; :: thesis: ( k in dom s implies ex b1, b2 being bag of 0 st

( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) )

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: ex b1, b2 being bag of 0 st

( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) )

then A22: ( 1 <= k & k <= 1 ) by A16, FINSEQ_3:25;

then A23: k = 1 by XXREAL_0:1;

take b1 = b1; :: thesis: ex b2 being bag of 0 st

( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) )

take b2 = b2; :: thesis: ( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) )

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: s /. k = (Px . b1) * (Py . b2)

thus s /. k = s . 1 by A21, A23, PARTFUN1:def 6

.= (Px . b1) * (Py . b2) by A19, A20, FINSEQ_1:40 ; :: thesis: verum

end;set b2 = {} ;

let k be Element of NAT ; :: thesis: ( k in dom s implies ex b1, b2 being bag of 0 st

( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) )

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: ex b1, b2 being bag of 0 st

( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) )

then A22: ( 1 <= k & k <= 1 ) by A16, FINSEQ_3:25;

then A23: k = 1 by XXREAL_0:1;

take b1 = b1; :: thesis: ex b2 being bag of 0 st

( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) )

take b2 = b2; :: thesis: ( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) )

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: s /. k = (Px . b1) * (Py . b2)

thus s /. k = s . 1 by A21, A23, PARTFUN1:def 6

.= (Px . b1) * (Py . b2) by A19, A20, FINSEQ_1:40 ; :: thesis: verum

ex b1, b2 being bag of 0 st

( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) ; :: thesis: verum

hence (P . x) * (P . y) = P . (x * y) by POLYNOM1:def 11; :: thesis: verum

take P ; :: thesis: P is RingIsomorphism

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: for x1, x2 being object st x1 in dom P & x2 in dom P & P . x1 = P . x2 holds

x1 = x2

then
P is one-to-one
by FUNCT_1:def 4;x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom P & x2 in dom P & P . x1 = P . x2 implies x1 = x2 )

assume that

A30: x1 in dom P and

A31: x2 in dom P ; :: thesis: ( P . x1 = P . x2 implies x1 = x2 )

assume P . x1 = P . x2 ; :: thesis: x1 = x2

then (Bags {}) --> x1 = P . x2 by A2, A30;

then (Bags {}) --> x1 = (Bags {}) --> x2 by A2, A31;

hence x1 = x2 by FUNCT_4:6; :: thesis: verum

end;assume that

A30: x1 in dom P and

A31: x2 in dom P ; :: thesis: ( P . x1 = P . x2 implies x1 = x2 )

assume P . x1 = P . x2 ; :: thesis: x1 = x2

then (Bags {}) --> x1 = P . x2 by A2, A30;

then (Bags {}) --> x1 = (Bags {}) --> x2 by A2, A31;

hence x1 = x2 by FUNCT_4:6; :: thesis: verum

then P is RingMonomorphism by A28;

hence P is RingIsomorphism by A29; :: thesis: verum