let R be non empty add-cancelable add-associative right_zeroed well-unital distributive associative commutative left_zeroed doubleLoopStr ; :: thesis: for a being Element of R holds {a} -Ideal = { (a * r) where r is Element of R : verum }
let a be Element of R; :: thesis: {a} -Ideal = { (a * r) where r is Element of R : verum }
set A = {a};
reconsider a9 = a as Element of {a} by TARSKI:def 1;
set M = { (Sum s) where s is LinearCombination of {a} : verum } ;
set N = { (a * r) where r is Element of R : verum } ;
A1: for u being object st u in { (Sum s) where s is LinearCombination of {a} : verum } holds
u in { (a * r) where r is Element of R : verum }

proof

let u be object ; :: thesis: ( u in { (Sum s) where s is LinearCombination of {a} : verum } implies u in { (a * r) where r is Element of R : verum } )
assume u in { (Sum s) where s is LinearCombination of {a} : verum } ; :: thesis: u in { (a * r) where r is Element of R : verum }
then consider s being LinearCombination of {a} such that
A2: u = Sum s ;
consider f being sequence of the carrier of R such that
A3: Sum s = f . (len s) and
A4: f . 0 = 0. R and
A5: for j being Nat
for v being Element of R st j < len s & v = s . (j + 1) holds
f . (j + 1) = (f . j) + v by RLVECT_1:def 12;
defpred S₁[ Element of NAT ] means ex r being Element of R st f . $1 = a * r;

A6: now :: thesis: for j being Element of NAT st 0 <= j & j < len s & S₁[j] holds
S₁[j + 1]

let j be Element of NAT ; :: thesis: ( 0 <= j & j < len s & S₁[j] implies S₁[j + 1] )
assume that
0 <= j and
A7: j < len s ; :: thesis: ( S₁[j] implies S₁[j + 1] )
thus ( S₁[j] implies S₁[j + 1] ) :: thesis: verum

proof

assume ex r being Element of R st f . j = a * r ; :: thesis: S₁[j + 1]
then consider r1 being Element of R such that
A8: f . j = a * r1 ;
( 0 + 1 <= j + 1 & j + 1 <= len s ) by A7, NAT_1:13;
then j + 1 in Seg (len s) by FINSEQ_1:1;
then A9: j + 1 in dom s by FINSEQ_1:def 3;
then consider r2, r3 being Element of R, a9 being Element of {a} such that
A10: s /. (j + 1) = (r2 * a9) * r3 by Def8;
s . (j + 1) = s /. (j + 1) by A9, PARTFUN1:def 6;
then f . (j + 1) = (f . j) + (s /. (j + 1)) by A5, A7;
then f . (j + 1) = (a * r1) + ((r2 * a) * r3) by A8, A10, TARSKI:def 1
.= (a * r1) + (a * (r2 * r3)) by GROUP_1:def 3
.= a * (r1 + (r2 * r3)) by VECTSP_1:def 7 ;
hence S₁[j + 1] ; :: thesis: verum

end;

end;

f . 0 = a * (0. R) by A4, BINOM:2;
then A11: S₁[ 0 ] ;
for k being Element of NAT st 0 <= k & k <= len s holds
S₁[k] from INT_1:sch 7(A11, A6);
then ex r being Element of R st Sum s = a * r by A3;
hence u in { (a * r) where r is Element of R : verum } by A2; :: thesis: verum

end;

A12: now :: thesis: for x being object holds
( ( x in {a} -Ideal implies x in { (Sum s) where s is LinearCombination of {a} : verum } ) & ( x in { (Sum s) where s is LinearCombination of {a} : verum } implies x in {a} -Ideal ) )

let x be object ; :: thesis: ( ( x in {a} -Ideal implies x in { (Sum s) where s is LinearCombination of {a} : verum } ) & ( x in { (Sum s) where s is LinearCombination of {a} : verum } implies x in {a} -Ideal ) )

hereby :: thesis: ( x in { (Sum s) where s is LinearCombination of {a} : verum } implies x in {a} -Ideal )

assume x in {a} -Ideal ; :: thesis: x in { (Sum s) where s is LinearCombination of {a} : verum }
then x in {a} -RightIdeal by Th63;
then consider f being RightLinearCombination of {a} such that
A13: x = Sum f by Th62;
f is LinearCombination of {a} by Th28;
hence x in { (Sum s) where s is LinearCombination of {a} : verum } by A13; :: thesis: verum

end;

assume x in { (Sum s) where s is LinearCombination of {a} : verum } ; :: thesis: x in {a} -Ideal
then ex s being LinearCombination of {a} st x = Sum s ;
hence x in {a} -Ideal by Th60; :: thesis: verum

end;

for u being object st u in { (a * r) where r is Element of R : verum } holds
u in { (Sum s) where s is LinearCombination of {a} : verum }

proof

let u be object ; :: thesis: ( u in { (a * r) where r is Element of R : verum } implies u in { (Sum s) where s is LinearCombination of {a} : verum } )
assume u in { (a * r) where r is Element of R : verum } ; :: thesis: u in { (Sum s) where s is LinearCombination of {a} : verum }
then consider r being Element of R such that
A14: u = a * r ;
set s = <*(a * r)*>;
for i being set st i in dom <*(a * r)*> holds
ex r, t being Element of R ex a being Element of {a} st <*(a * r)*> /. i = (r * a) * t

proof

let i be set ; :: thesis: ( i in dom <*(a * r)*> implies ex r, t being Element of R ex a being Element of {a} st <*(a * r)*> /. i = (r * a) * t )
A15: len <*(a * r)*> = 1 by FINSEQ_1:40;
assume i in dom <*(a * r)*> ; :: thesis: ex r, t being Element of R ex a being Element of {a} st <*(a * r)*> /. i = (r * a) * t
then i in {1} by A15, FINSEQ_1:2, FINSEQ_1:def 3;
then i = 1 by TARSKI:def 1;
then <*(a * r)*> /. i = a * r by FINSEQ_4:16
.= (r * a9) * (1. R) ;
hence ex r, t being Element of R ex a being Element of {a} st <*(a * r)*> /. i = (r * a) * t ; :: thesis: verum

end;

then reconsider s = <*(a * r)*> as LinearCombination of {a} by Def8;
Sum s = a * r by BINOM:3;
hence u in { (Sum s) where s is LinearCombination of {a} : verum } by A14; :: thesis: verum

end;

then { (Sum s) where s is LinearCombination of {a} : verum } = { (a * r) where r is Element of R : verum } by A1, TARSKI:2;
hence {a} -Ideal = { (a * r) where r is Element of R : verum } by A12, TARSKI:2; :: thesis: verum