let R be non empty non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; :: thesis:
let X be infinite Ordinal; :: thesis:
assume A1: Polynom-Ring X,R is Noetherian ; :: thesis:
set tcR = the carrier of R;
set tcPR = the carrier of (Polynom-Ring X,R);
A2: NAT c= X by CARD_3:102;
set S = { (1_1 n,R) where n is Element of X : n in NAT } ;
A3: { (1_1 n,R) where n is Element of X : n in NAT } c= the carrier of (Polynom-Ring X,R)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { (1_1 n,R) where n is Element of X : n in NAT } ; :: thesis:
then consider n being Element of X such that
A4: ( x = 1_1 n,R & n in NAT ) ;
thus x in the carrier of (Polynom-Ring X,R) by A4, POLYNOM1:def 27; :: thesis:

end;

0 in NAT ;
then reconsider 0X = 0 as Element of X by A2;
1_1 0X,R in { (1_1 n,R) where n is Element of X : n in NAT } ;
then reconsider S = { (1_1 n,R) where n is Element of X : n in NAT } as non empty Subset of the carrier of (Polynom-Ring X,R) by A3;
consider C being non empty finite Subset of the carrier of (Polynom-Ring X,R) such that
A5: C c= S and
A6: C -Ideal = S -Ideal by A1, IDEAL_1:99;
deffunc H₁( set ) -> set = $1;
deffunc H₂( Element of X) -> Series of X,R = 1_1 $1,R;
set CN = { H₁(n) where n is Element of X : H₂(n) in C } ;
A7: C is finite ;
A8: for d1, d2 being Element of X st H₂(d1) = H₂(d2) holds
d1 = d2 by Th14;
A9: { H₁(n) where n is Element of X : H₂(n) in C } is finite from FUNCT_7:sch 2(A7, A8);
consider c being Element of C;
c in C ;
then c in S by A5;
then consider cn being Element of X such that
A10: ( c = 1_1 cn,R & cn in NAT ) ;
reconsider cn = cn as Element of NAT by A10;
A11: cn in { H₁(n) where n is Element of X : H₂(n) in C } by A10;
{ H₁(n) where n is Element of X : H₂(n) in C } c= NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { H₁(n) where n is Element of X : H₂(n) in C } ; :: thesis:
then consider n being Element of X such that
A12: ( x = n & 1_1 n,R in C ) ;
1_1 n,R in S by A5, A12;
then consider m being Element of X such that
A13: ( 1_1 n,R = 1_1 m,R & m in NAT ) ;
thus x in NAT by A12, A13, Th14; :: thesis:

end;

then reconsider CN = { H₁(n) where n is Element of X : H₂(n) in C } as non empty finite Subset of NAT by A9, A11;
reconsider mm = max CN as Element of NAT by ORDINAL1:def 13;
reconsider m1 = mm + 1 as Element of NAT ;
m1 in NAT ;
then reconsider m2 = m1 as Element of X by A2;
( 1_1 m2,R in S & S c= S -Ideal ) by IDEAL_1:def 15;
then consider lc being LinearCombination of C such that
A14: 1_1 m2,R = Sum lc by A6, IDEAL_1:60;
reconsider f0 = X --> (0. R) as Function of X,the carrier of R ;
reconsider ev = f0 +* m2,(1_ R) as Function of X,R ;
dom (X --> (0. R)) = X by FUNCOP_1:19;
then A15: ev . m2 = 1_ R by FUNCT_7:33;
A16: Support (1_1 m2,R) = {(UnitBag m2)} by Th13;
A17: (Polynom-Evaluation X,R,ev) . (1_1 m2,R) = eval (1_1 m2,R),ev by POLYNOM2:def 5
.= ((1_1 m2,R) . (UnitBag m2)) * (eval (UnitBag m2),ev) by A16, POLYNOM2:21
.= (1_ R) * (eval (UnitBag m2),ev) by Th12
.= (1_ R) * (ev . m2) by Th11
.= 1_ R by A15, GROUP_1:def 5 ;
the carrier of R c= the carrier of R ;
then reconsider cR = the carrier of R as non empty Subset of the carrier of R ;
consider E being FinSequence of [:the carrier of (Polynom-Ring X,R),the carrier of (Polynom-Ring X,R),the carrier of (Polynom-Ring X,R):] such that
A18: E represents lc by IDEAL_1:35;
set P = Polynom-Evaluation X,R,ev;
deffunc H₃( Nat) -> Element of the carrier of R = (((Polynom-Evaluation X,R,ev) . ((E /. $1) `1 )) * ((Polynom-Evaluation X,R,ev) . ((E /. $1) `2 ))) * ((Polynom-Evaluation X,R,ev) . ((E /. $1) `3 ));
consider LC being FinSequence of the carrier of R such that
A19: len LC = len lc and
A20: for k being Nat st k in dom LC holds
LC . k = H₃(k) from FINSEQ_2:sch 1();
A21: dom LC = Seg (len lc) by A19, FINSEQ_1:def 3;

now

let i be set ; :: thesis:
assume A22: i in dom LC ; :: thesis:
then reconsider k = i as Element of NAT ;
A23: k in Seg (len lc) by A19, A22, FINSEQ_1:def 3;
reconsider u = (Polynom-Evaluation X,R,ev) . ((E /. k) `1 ), v = (Polynom-Evaluation X,R,ev) . ((E /. k) `3 ) as Element of R ;
reconsider a = (Polynom-Evaluation X,R,ev) . ((E /. k) `2 ) as Element of cR ;
take u = u; :: thesis:
take v = v; :: thesis:
take a = a; :: thesis:
thus LC /. i = LC . k by A22, PARTFUN1:def 8
.= (u * a) * v by A20, A23, A21 ; :: thesis:

end;

then reconsider LC = LC as LinearCombination of cR by IDEAL_1:def 9;

A24: now

let i be Element of NAT ; :: thesis:
assume A25: i in dom LC ; :: thesis:
then A26: i in dom lc by A19, FINSEQ_3:31;
A27: i in Seg (len lc) by A19, A25, FINSEQ_1:def 3;
reconsider y = (E /. i) `2 as Element of C by A18, A26, IDEAL_1:def 12;
y in C ;
then y in S by A5;
then consider n being Element of X such that
A28: ( y = 1_1 n,R & n in NAT ) ;
A29: n in CN by A28;

now

assume m2 in CN ; :: thesis:
then (max CN) + 1 <= max CN by XXREAL_2:def 8;
hence contradiction by XREAL_1:31; :: thesis:

end;

then A30: ev . n = (X --> (0. R)) . n by A29, FUNCT_7:34
.= 0. R by FUNCOP_1:13 ;
A31: Support (1_1 n,R) = {(UnitBag n)} by Th13;
A32: (Polynom-Evaluation X,R,ev) . (1_1 n,R) = eval (1_1 n,R),ev by POLYNOM2:def 5
.= ((1_1 n,R) . (UnitBag n)) * (eval (UnitBag n),ev) by A31, POLYNOM2:21
.= (1_ R) * (eval (UnitBag n),ev) by Th12
.= (1_ R) * (ev . n) by Th11
.= 0. R by A30, VECTSP_1:36 ;
thus LC . i = (((Polynom-Evaluation X,R,ev) . ((E /. i) `1 )) * ((Polynom-Evaluation X,R,ev) . ((E /. i) `2 ))) * ((Polynom-Evaluation X,R,ev) . ((E /. i) `3 )) by A20, A27, A21
.= (0. R) * ((Polynom-Evaluation X,R,ev) . ((E /. i) `3 )) by A28, A32, VECTSP_1:36
.= 0. R by VECTSP_1:36 ; :: thesis:

end;

for k being set st k in dom LC holds
LC . k = (((Polynom-Evaluation X,R,ev) . ((E /. k) `1 )) * ((Polynom-Evaluation X,R,ev) . ((E /. k) `2 ))) * ((Polynom-Evaluation X,R,ev) . ((E /. k) `3 )) by A20;
then (Polynom-Evaluation X,R,ev) . (Sum lc) = Sum LC by A18, A19, Th24
.= 0. R by A24, POLYNOM3:1 ;
hence contradiction by A14, A17, POLYNOM1:27; :: thesis: