let R be non empty add-cancelable add-associative right_zeroed well-unital distributive associative left_zeroed Noetherian doubleLoopStr ; :: thesis: for B being non empty Subset of R ex C being non empty finite Subset of R st
( C c= B & C -Ideal = B -Ideal )
let B be non empty Subset of R; :: thesis: ex C being non empty finite Subset of R st
( C c= B & C -Ideal = B -Ideal )
defpred S₁[ object , object ] means ex cL being non empty LinearCombination of B st
( $1 = Sum cL & ex fsB being FinSequence of B st
( dom fsB = dom cL & $2 = rng fsB & ( for i being Nat st i in dom cL holds
ex u, v being Element of R st cL /. i = (u * (fsB /. i)) * v ) ) );
B -Ideal is finitely_generated by Def26;
then consider D being non empty finite Subset of R such that
A1: D -Ideal = B -Ideal ;
A2: D c= B -Ideal by A1, Def14;
A3: for e being object st e in D holds
ex u being object st
( u in bool B & S₁[e,u] )

proof

let e be object ; :: thesis: ( e in D implies ex u being object st
( u in bool B & S₁[e,u] ) )
assume e in D ; :: thesis: ex u being object st
( u in bool B & S₁[e,u] )
then consider cL being LinearCombination of B such that
A4: e = Sum cL by A2, Th60;

per cases ( not cL is empty or cL is empty ) ;

suppose A5: not cL is empty ; :: thesis: ex u being object st
( u in bool B & S₁[e,u] )

defpred S₂[ set , Element of B] means ex u, v being Element of R st cL /. $1 = (u * $2) * v;

A6: now :: thesis: for k being Nat st k in Seg (len cL) holds
ex d being Element of B st S₂[k,d]

let k be Nat; :: thesis: ( k in Seg (len cL) implies ex d being Element of B st S₂[k,d] )
assume k in Seg (len cL) ; :: thesis: ex d being Element of B st S₂[k,d]
then k in dom cL by FINSEQ_1:def 3;
then consider u, v being Element of R, a being Element of B such that
A7: cL /. k = (u * a) * v by Def8;
take d = a; :: thesis: S₂[k,d]
thus S₂[k,d] by A7; :: thesis: verum

end;

consider fsB being FinSequence of B such that
A8: ( dom fsB = Seg (len cL) & ( for k being Nat st k in Seg (len cL) holds
S₂[k,fsB /. k] ) ) from RECDEF_1:sch 17(A6);
take u = rng fsB; :: thesis: ( u in bool B & S₁[e,u] )
thus u in bool B ; :: thesis: S₁[e,u]
dom cL = Seg (len cL) by FINSEQ_1:def 3;
hence S₁[e,u] by A4, A5, A8; :: thesis: verum

end;

suppose A9: cL is empty ; :: thesis: ex u being object st
( u in bool B & S₁[e,u] )

set b = the Element of B;
set kL = <*(((0. R) * the Element of B) * (0. R))*>;

now :: thesis: for i being set st i in dom <*(((0. R) * the Element of B) * (0. R))*> holds
ex u, v being Element of the carrier of R ex b being Element of B st <*(((0. R) * the Element of B) * (0. R))*> /. i = (u * b) * v

let i be set ; :: thesis: ( i in dom <*(((0. R) * the Element of B) * (0. R))*> implies ex u, v being Element of the carrier of R ex b being Element of B st <*(((0. R) * the Element of B) * (0. R))*> /. i = (u * b) * v )
assume A10: i in dom <*(((0. R) * the Element of B) * (0. R))*> ; :: thesis: ex u, v being Element of the carrier of R ex b being Element of B st <*(((0. R) * the Element of B) * (0. R))*> /. i = (u * b) * v
take u = 0. R; :: thesis: ex v being Element of the carrier of R ex b being Element of B st <*(((0. R) * the Element of B) * (0. R))*> /. i = (u * b) * v
take v = 0. R; :: thesis: ex b being Element of B st <*(((0. R) * the Element of B) * (0. R))*> /. i = (u * b) * v
take b = the Element of B; :: thesis: <*(((0. R) * the Element of B) * (0. R))*> /. i = (u * b) * v
i in Seg (len <*(((0. R) * the Element of B) * (0. R))*>) by A10, FINSEQ_1:def 3;
then i in {1} by FINSEQ_1:2, FINSEQ_1:40;
then i = 1 by TARSKI:def 1;
hence <*(((0. R) * the Element of B) * (0. R))*> /. i = (u * b) * v by FINSEQ_4:16; :: thesis: verum

end;

then reconsider kL = <*(((0. R) * the Element of B) * (0. R))*> as non empty LinearCombination of B by Def8;
cL = <*> the carrier of R by A9;
then A11: e = 0. R by A4, RLVECT_1:43
.= ((0. R) * the Element of B) * (0. R) by BINOM:2
.= Sum kL by BINOM:3 ;
defpred S₂[ Nat, Element of B] means ex u, v being Element of R st kL /. $1 = (u * $2) * v;

A12: now :: thesis: for k being Nat st k in Seg (len kL) holds
ex b being Element of B st S₂[k,b]

let k be Nat; :: thesis: ( k in Seg (len kL) implies ex b being Element of B st S₂[k,b] )
assume A13: k in Seg (len kL) ; :: thesis: ex b being Element of B st S₂[k,b]
take b = the Element of B; :: thesis: S₂[k,b]
k in {1} by A13, FINSEQ_1:2, FINSEQ_1:40;
then k = 1 by TARSKI:def 1;
hence S₂[k,b] by FINSEQ_4:16; :: thesis: verum

end;

consider fsB being FinSequence of B such that
A14: ( dom fsB = Seg (len kL) & ( for k being Nat st k in Seg (len kL) holds
S₂[k,fsB /. k] ) ) from RECDEF_1:sch 17(A12);
take u = rng fsB; :: thesis: ( u in bool B & S₁[e,u] )
thus u in bool B ; :: thesis: S₁[e,u]
dom kL = Seg (len kL) by FINSEQ_1:def 3;
hence S₁[e,u] by A11, A14; :: thesis: verum

end;

end;

end;

consider f being Function of D,(bool B) such that
A15: for e being object st e in D holds
S₁[e,f . e] from FUNCT_2:sch 1(A3);

A16: now :: thesis: for r being set st r in rng f holds
r is finite

let r be set ; :: thesis: ( r in rng f implies r is finite )
assume r in rng f ; :: thesis: r is finite
then consider x being object such that
A17: ( x in dom f & r = f . x ) by FUNCT_1:def 3;
ex cL being non empty LinearCombination of B st
( x = Sum cL & ex fsB being FinSequence of B st
( dom fsB = dom cL & r = rng fsB & ( for i being Nat st i in dom cL holds
ex u, v being Element of R st cL /. i = (u * (fsB /. i)) * v ) ) ) by A15, A17;
hence r is finite ; :: thesis: verum

end;

reconsider rf = rng f as Subset-Family of B ;
reconsider C = union rf as Subset of B ;
consider r being object such that
A18: r in rng f by XBOOLE_0:def 1;
consider x being object such that
A19: ( x in dom f & r = f . x ) by A18, FUNCT_1:def 3;
reconsider r = r as set by TARSKI:1;
ex cL being non empty LinearCombination of B st
( x = Sum cL & ex fsB being FinSequence of B st
( dom fsB = dom cL & r = rng fsB & ( for i being Nat st i in dom cL holds
ex u, v being Element of R st cL /. i = (u * (fsB /. i)) * v ) ) ) by A15, A19;
then not r is empty by RELAT_1:42;
then ex x being object st x in r ;
then reconsider C = C as non empty finite Subset of R by A18, A16, FINSET_1:7, TARSKI:def 4, XBOOLE_1:1;

now :: thesis: for d being object st d in D holds
d in C -Ideal

let d be object ; :: thesis: ( d in D implies d in C -Ideal )
assume A20: d in D ; :: thesis: d in C -Ideal
then consider cL being non empty LinearCombination of B such that
A21: d = Sum cL and
A22: ex fsB being FinSequence of B st
( dom fsB = dom cL & f . d = rng fsB & ( for i being Nat st i in dom cL holds
ex u, v being Element of R st cL /. i = (u * (fsB /. i)) * v ) ) by A15;
d in dom f by A20, FUNCT_2:def 1;
then f . d in rng f by FUNCT_1:def 3;
then A23: f . d c= C by ZFMISC_1:74;

now :: thesis: for i being set st i in dom cL holds
ex u, v being Element of R ex a being Element of C st cL /. i = (u * a) * v

let i be set ; :: thesis: ( i in dom cL implies ex u, v being Element of R ex a being Element of C st cL /. i = (u * a) * v )
consider fsB being FinSequence of B such that
A24: dom fsB = dom cL and
A25: f . d = rng fsB and
A26: for i being Nat st i in dom cL holds
ex u, v being Element of R st cL /. i = (u * (fsB /. i)) * v by A22;
assume A27: i in dom cL ; :: thesis: ex u, v being Element of R ex a being Element of C st cL /. i = (u * a) * v
then fsB /. i = fsB . i by A24, PARTFUN1:def 6;
then A28: fsB /. i in f . d by A27, A24, A25, FUNCT_1:def 3;
ex u, v being Element of R st cL /. i = (u * (fsB /. i)) * v by A27, A26;
hence ex u, v being Element of R ex a being Element of C st cL /. i = (u * a) * v by A23, A28; :: thesis: verum

end;

then reconsider cL9 = cL as LinearCombination of C by Def8;
d = Sum cL9 by A21;
hence d in C -Ideal by Th60; :: thesis: verum

end;

then D c= C -Ideal ;
then D -Ideal c= (C -Ideal) -Ideal by Th57;
then A29: B -Ideal c= C -Ideal by A1, Th44;
take C ; :: thesis: ( C c= B & C -Ideal = B -Ideal )
C -Ideal c= B -Ideal by Th57;
hence ( C c= B & C -Ideal = B -Ideal ) by A29; :: thesis: verum