let R be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative left_zeroed doubleLoopStr ; :: thesis:
let A be non empty Subset of R; :: thesis:
let a be Element of R; :: thesis:
assume a in A -Ideal ; :: thesis:
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:
assume u in {a} -Ideal ; :: thesis:
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

let i be set ; :: thesis:
assume A4: i in dom (s * r) ; :: thesis:
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:

end;