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 LinearCombination 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 LinearCombination 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 LinearCombination of P st
( P c= M & o = Sum L ) )

A: now :: thesis: ( o in M -Ideal implies ex P being non empty finite Subset of R ex L being LinearCombination 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 LinearCombination of P st
( P c= M & o = Sum L )
then consider P being non empty finite Subset of R, L being LeftLinearCombination of P such that
A1: ( P c= M & o = Sum L ) by ideal1;
L is LinearCombination of P by IDEAL_1:25;
hence ex P being non empty finite Subset of R ex L being LinearCombination of P st
( P c= M & o = Sum L ) by A1; :: thesis: verum

end;

now :: thesis: ( ex P being non empty finite Subset of R ex L being LinearCombination 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 LinearCombination 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 LinearCombination of P such that
A2: ( P c= M & o = Sum L ) ;
L is LeftLinearCombination of P by IDEAL_1:31;
hence o in M -Ideal by A2, ideal1; :: thesis: verum

end;

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