deffunc H1( object ) -> Element of bool [:(),{\$1}:] = () --> \$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 = H1(x) from
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 ) )
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 ) )
hereby :: thesis: ( y in the carrier of (Polynom-Ring (0,R)) implies y in rng P )
assume 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 ;
reconsider x = x as Element of R by A3;
reconsider y9 = () --> x as Function of (),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;
assume y in the carrier of (Polynom-Ring (0,R)) ; :: thesis: y in rng P
then reconsider y9 = y as Function of (),R by POLYNOM1:def 11;
dom y9 = Bags {} by FUNCT_2:def 1;
then rng y9 = {(y9 . {})} by ;
then y9 . {} in rng y9 by TARSKI:def 1;
then reconsider x = y9 . {} as Element of R ;
y9 = () --> (y9 . {}) ;
then y = P . x by A2;
hence y in rng P by ; :: thesis: verum
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 ;
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)
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;
now :: thesis: for z being bag of 0 holds Pxy . z = (Px . z) + (Py . z)
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 = (() --> y) . z by A2
.= y by ;
A12: Px . z = (() --> x) . z by A2
.= x by ;
Pxy . z = (() --> (x + y)) . z by A2
.= x + y by ;
hence Pxy . z = (Px . z) + (Py . z) by ; :: thesis: verum
end;
then Pxy = Px + Py by POLYNOM1:16;
hence (P . x) + (P . y) = P . (x + y) by POLYNOM1:def 11; :: thesis: verum
end;
then A13: P is additive ;
now :: thesis: for x, y being Element of R holds (P . x) * (P . y) = P . (x * y)
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;
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 () & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of 0 st
( () /. 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 () & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of 0 st
( () /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) ) )

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

A14: b in Bags {} by PRE_POLY:def 12;
thus Pxy . b = (() --> (x * y)) . b by A2
.= x * y by
.= Sum s by RLVECT_1:44 ; :: thesis: ( len s = len () & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of 0 st
( () /. 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 () by ; :: thesis: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of 0 st
( () /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) )

A17: len () = 1 by ;
now :: thesis: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of 0 st
( () /. 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
( () /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) )

A18: {} in Bags {} by ;
then reconsider b1 = {} , b2 = {} as bag of 0 ;
A19: Px . b1 = (() --> x) . b1 by A2
.= x by ;
A20: Py . b2 = (() --> y) . b2 by A2
.= y by ;
assume A21: k in dom s ; :: thesis: ex b1, b2 being bag of 0 st
( () /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) )

then A22: ( 1 <= k & k <= 1 ) by ;
then A23: k = 1 by XXREAL_0:1;
take b1 = b1; :: thesis: ex b2 being bag of 0 st
( () /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) )

take b2 = b2; :: thesis: ( () /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) )
k in dom () by ;
hence () /. k = () . 1 by
.= <*b1,b2*> by ;
:: thesis: s /. k = (Px . b1) * (Py . b2)
thus s /. k = s . 1 by
.= (Px . b1) * (Py . b2) by ; :: thesis: verum
end;
hence for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of 0 st
( () /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) ; :: thesis: verum
end;
then Pxy = Px *' Py by POLYNOM1:def 10;
hence (P . x) * (P . y) = P . (x * y) by POLYNOM1:def 11; :: thesis: verum
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
.= ( --> (0. R)) +* ({},(1_ R)) by
.= ( --> (0. R)) +* ({} .--> (1_ R)) by
.= --> (1_ R) by
.= P . (1_ R) by ;
then P is unity-preserving by GROUP_1:def 13;
then A28: P is RingHomomorphism by ;
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
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 ;
then (Bags {}) --> x1 = () --> x2 by ;
hence x1 = x2 by FUNCT_4:6; :: thesis: verum
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: verum