let R be comRing; :: thesis:
let a be Element of R; :: thesis:
set M = { (a * r) where r is Element of R : verum } ;

let u be object ; :: thesis:
assume u in { (a * r) where r is Element of R : verum } ; :: thesis:
then ex r being Element of R st u = a * r ;
hence u in the carrier of R ; :: thesis:

end;

a * (1. R) in { (a * r) where r is Element of R : verum } ;
then reconsider M = { (a * r) where r is Element of R : verum } as non empty Subset of R by A1, TARSKI:def 3;
reconsider M = M as non empty Subset of R ;

A2: now :: thesis:

let b, c be Element of R; :: thesis:
assume that
A3: b in M and
A4: c in M ; :: thesis:
consider r being Element of R such that
A5: a * r = b by A3;
consider s being Element of R such that
A6: a * s = c by A4;
b + c = a * (r + s) by A5, A6, VECTSP_1:def 7;
hence b + c in M ; :: thesis:

end;

A7: now :: thesis:

let s, b be Element of R; :: thesis:
assume b in M ; :: thesis:
then consider r being Element of R such that
A8: a * r = b ;
s * b = (s * r) * a by A8, GROUP_1:def 3;
hence s * b in M ; :: thesis:

end;

now :: thesis:

let s, b be Element of R; :: thesis:
assume b in M ; :: thesis:
then consider r being Element of R such that
A9: a * r = b ;
b * s = a * (r * s) by A9, GROUP_1:def 3;
hence b * s in M ; :: thesis:

end;

hence { (a * r) where r is Element of R : verum } is Ideal of R by A2, A7, Def1, Def2, Def3; :: thesis: