let R be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative left_zeroed doubleLoopStr ; :: thesis: for A being non empty Subset of R
for a being Element of R st a in A -Ideal holds
{a} -Ideal c= A -Ideal
let A be non empty Subset of R; :: thesis: for a being Element of R st a in A -Ideal holds
{a} -Ideal c= A -Ideal
let a be Element of R; :: thesis: ( a in A -Ideal implies {a} -Ideal c= A -Ideal )
assume a in A -Ideal ; :: thesis: {a} -Ideal c= A -Ideal
then consider s being LinearCombination of A such that
A1: a = Sum s by Th60;
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in {a} -Ideal or u in A -Ideal )
assume u in {a} -Ideal ; :: thesis: u in A -Ideal
then u in { (a * r) where r is Element of R : verum } by Th64;
then consider r being Element of R such that
A2: u = a * r ;
set t = s * r;
A3: dom s = dom (s * r) by POLYNOM1:def 2;
for i being set st i in dom (s * r) holds
ex u, v being Element of R ex a being Element of A st (s * r) /. i = (u * a) * v

proof

let i be set ; :: thesis: ( i in dom (s * r) implies ex u, v being Element of R ex a being Element of A st (s * r) /. i = (u * a) * v )
assume A4: i in dom (s * r) ; :: thesis: ex u, v being Element of R ex a being Element of A st (s * r) /. i = (u * a) * v
then consider u, v being Element of R, b being Element of A such that
A5: s /. i = (u * b) * v by A3, Def8;
(s * r) /. i = ((u * b) * v) * r by A3, A4, A5, POLYNOM1:def 2
.= (u * b) * (v * r) by GROUP_1:def 3 ;
hence ex u, v being Element of R ex a being Element of A st (s * r) /. i = (u * a) * v ; :: thesis: verum

end;

then A6: s * r is LinearCombination of A by Def8;
Sum (s * r) = u by A1, A2, BINOM:5;
hence u in A -Ideal by A6, Th60; :: thesis: verum