let R be non degenerated comRing; :: thesis: for M being non empty Subset of R
for o being object holds
( o in M -Ideal iff ex P being non empty finite Subset of R ex L being LeftLinearCombination of P st
( P c= M & o = Sum L ) )
let M be non empty Subset of R; :: thesis: for o being object holds
( o in M -Ideal iff ex P being non empty finite Subset of R ex L being LeftLinearCombination of P st
( P c= M & o = Sum L ) )
let o be object ; :: thesis: ( o in M -Ideal iff ex P being non empty finite Subset of R ex L being LeftLinearCombination of P st
( P c= M & o = Sum L ) )

A: now :: thesis: ( ex P being non empty finite Subset of R ex L being LeftLinearCombination of P st
( P c= M & o = Sum L ) implies o in M -Ideal )

assume ex P being non empty finite Subset of R ex L being LeftLinearCombination of P st
( P c= M & o = Sum L ) ; :: thesis: o in M -Ideal
then consider P being non empty finite Subset of R, L being LeftLinearCombination of P such that
A1: ( P c= M & o = Sum L ) ;

now :: thesis: for i being set st i in dom L holds
ex u being Element of R ex a being Element of M st L /. i = u * a

let i be set ; :: thesis: ( i in dom L implies ex u being Element of R ex a being Element of M st L /. i = u * a )
assume i in dom L ; :: thesis: ex u being Element of R ex a being Element of M st L /. i = u * a
then consider u being Element of R, a being Element of P such that
A2: L /. i = u * a by IDEAL_1:def 9;
a is Element of M by A1;
hence ex u being Element of R ex a being Element of M st L /. i = u * a by A2; :: thesis: verum

end;

then L is LeftLinearCombination of M by IDEAL_1:def 9;
then o in M -LeftIdeal by A1, IDEAL_1:61;
hence o in M -Ideal by IDEAL_1:63; :: thesis: verum

end;

defpred S₁[ Nat] means for L being LinearCombination of M st len L = $1 holds
ex P being non empty finite Subset of R ex L1 being LeftLinearCombination of P st
( P c= M & Sum L1 = Sum L );
IA: S₁[ 0 ]

proof

now :: thesis: for L being LinearCombination of M st len L = 0 holds
ex P being non empty finite Subset of R ex L1 being LeftLinearCombination of P st
( P c= M & Sum L1 = Sum L )

let L be LinearCombination of M; :: thesis: ( len L = 0 implies ex P being non empty finite Subset of R ex L1 being LeftLinearCombination of P st
( P c= M & Sum L1 = Sum L ) )
assume len L = 0 ; :: thesis: ex P being non empty finite Subset of R ex L1 being LeftLinearCombination of P st
( P c= M & Sum L1 = Sum L )
then L = <*> the carrier of R ;
then I3: Sum L = 0. R by RLVECT_1:43;
set a = the Element of M;
set P = { the Element of M};
set K = <*((0. R) * the Element of M)*>;

now :: thesis: for u being object st u in { the Element of M} holds
u in M

let u be object ; :: thesis: ( u in { the Element of M} implies u in M )
assume u in { the Element of M} ; :: thesis: u in M
then u = the Element of M by TARSKI:def 1;
hence u in M ; :: thesis: verum

end;

then I4: { the Element of M} c= M ;
I5: Sum <*((0. R) * the Element of M)*> = Sum L by I3, RLVECT_1:44;

now :: thesis: for i being set st i in dom <*((0. R) * the Element of M)*> holds
ex u being Element of R ex a being Element of { the Element of M} st <*((0. R) * the Element of M)*> /. i = u * a

let i be set ; :: thesis: ( i in dom <*((0. R) * the Element of M)*> implies ex u being Element of R ex a being Element of { the Element of M} st <*((0. R) * the Element of M)*> /. i = u * a )
assume I6: i in dom <*((0. R) * the Element of M)*> ; :: thesis: ex u being Element of R ex a being Element of { the Element of M} st <*((0. R) * the Element of M)*> /. i = u * a
then i in Seg 1 by FINSEQ_1:38;
then I8: i = 1 by TARSKI:def 1, FINSEQ_1:2;
I7: (0. R) * the Element of M = <*((0. R) * the Element of M)*> . 1
.= <*((0. R) * the Element of M)*> /. 1 by I6, I8, PARTFUN1:def 6 ;
the Element of M in { the Element of M} by TARSKI:def 1;
hence ex u being Element of R ex a being Element of { the Element of M} st <*((0. R) * the Element of M)*> /. i = u * a by I7, I8; :: thesis: verum

end;

then <*((0. R) * the Element of M)*> is LeftLinearCombination of { the Element of M} by IDEAL_1:def 9;
hence ex P being non empty finite Subset of R ex L1 being LeftLinearCombination of P st
( P c= M & Sum L1 = Sum L ) by I4, I5; :: thesis: verum

end;

hence S₁[ 0 ] ; :: thesis: verum

end;

IS: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for L being LinearCombination of M st len L = k + 1 holds
ex P being non empty finite Subset of R ex L1 being LeftLinearCombination of P st
( P c= M & Sum L1 = Sum L )

let L be LinearCombination of M; :: thesis: ( len L = k + 1 implies ex P being non empty finite Subset of R ex L1 being LeftLinearCombination of P st
( P c= M & Sum L1 = Sum L ) )
assume I2: len L = k + 1 ; :: thesis: ex P being non empty finite Subset of R ex L1 being LeftLinearCombination of P st
( P c= M & Sum L1 = Sum L )
then L <> {} ;
then consider K being LinearCombination of M, a being Element of R such that
I3: ( L = K ^ <*a*> & <*a*> is LinearCombination of M ) by IDEAL_1:32;
I4: len L = (len K) + (len <*a*>) by I3, FINSEQ_1:22
.= (len K) + 1 by FINSEQ_1:39 ;
then consider Pk being non empty finite Subset of R, U being LeftLinearCombination of Pk such that
I6: ( Pk c= M & Sum U = Sum K ) by I2, IV;
1 <= len L by I2, NAT_1:11;
then len L in Seg (len L) ;
then I11: len L in dom L by FINSEQ_1:def 3;
then consider u, v being Element of R, b being Element of M such that
I7: L /. (len L) = (u * b) * v by IDEAL_1:def 8;
set P = Pk \/ {b};
set V = <*((u * v) * b)*>;

now :: thesis: for i being set st i in dom <*((u * v) * b)*> holds
ex u being Element of R ex a being Element of Pk \/ {b} st <*((u * v) * b)*> /. i = u * a

let i be set ; :: thesis: ( i in dom <*((u * v) * b)*> implies ex u being Element of R ex a being Element of Pk \/ {b} st <*((u * v) * b)*> /. i = u * a )
assume E1: i in dom <*((u * v) * b)*> ; :: thesis: ex u being Element of R ex a being Element of Pk \/ {b} st <*((u * v) * b)*> /. i = u * a
then i in Seg 1 by FINSEQ_1:38;
then E2: i = 1 by TARSKI:def 1, FINSEQ_1:2;
E3: (u * v) * b = <*((u * v) * b)*> . 1
.= <*((u * v) * b)*> /. 1 by E1, E2, PARTFUN1:def 6 ;
b in {b} by TARSKI:def 1;
then b in Pk \/ {b} by XBOOLE_0:def 3;
hence ex u being Element of R ex a being Element of Pk \/ {b} st <*((u * v) * b)*> /. i = u * a by E3, E2; :: thesis: verum

end;

then reconsider V = <*((u * v) * b)*> as LeftLinearCombination of Pk \/ {b} by IDEAL_1:def 9;
I8: U ^ V is LeftLinearCombination of Pk \/ {b} by XBOOLE_1:7, XBOOLE_1:12;

now :: thesis: for o being object st o in Pk \/ {b} holds
o in M

let o be object ; :: thesis: ( o in Pk \/ {b} implies b₁ in M )
assume o in Pk \/ {b} ; :: thesis: b₁ in M

per cases then ( o in Pk or o in {b} ) by XBOOLE_0:def 3;

suppose o in Pk ; :: thesis: b₁ in M

hence o in M by I6; :: thesis: verum

end;

suppose o in {b} ; :: thesis: b₁ in M

then o = b by TARSKI:def 1;
hence o in M ; :: thesis: verum

end;

end;

end;

then I9: Pk \/ {b} c= M ;
I10: a = L . (len L) by I3, I4, FINSEQ_1:42
.= L /. (len L) by I11, PARTFUN1:def 6
.= u * (b * v) by I7, GROUP_1:def 3
.= u * (v * b) by GROUP_1:def 12
.= (u * v) * b by GROUP_1:def 3 ;
Sum L = (Sum K) + (Sum <*a*>) by I3, RLVECT_1:41
.= Sum (U ^ V) by I10, I6, RLVECT_1:41 ;
hence ex P being non empty finite Subset of R ex L1 being LeftLinearCombination of P st
( P c= M & Sum L1 = Sum L ) by I8, I9; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);

now :: thesis: for o being object st o in M -Ideal holds
ex P being non empty finite Subset of R ex L being LeftLinearCombination of P st
( P c= M & o = Sum L )

let o be object ; :: thesis: ( o in M -Ideal implies ex P being non empty finite Subset of R ex L being LeftLinearCombination of P st
( P c= M & o = Sum L ) )
assume o in M -Ideal ; :: thesis: ex P being non empty finite Subset of R ex L being LeftLinearCombination of P st
( P c= M & o = Sum L )
then consider L being LinearCombination of M such that
C: o = Sum L by IDEAL_1:60;
consider n being Nat such that
H: n = len L ;
thus ex P being non empty finite Subset of R ex L being LeftLinearCombination of P st
( P c= M & o = Sum L ) by H, C, I; :: thesis: verum

end;

hence ( o in M -Ideal iff ex P being non empty finite Subset of R ex L being LeftLinearCombination of P st
( P c= M & o = Sum L ) ) by A; :: thesis: verum