set I = Image f;

now :: thesis: for v, w being Element of (Image f) holds v + w = w + v

let v, w be Element of (Image f); :: thesis: v + w = w + v
consider a being Element of R such that
A1: f . a = v by T6;
consider b being Element of R such that
A2: f . b = w by T6;
thus v + w = (f . a) + (f . b) by A1, A2, T5
.= w + v by A1, A2, T5 ; :: thesis: verum

end;

hence Image f is Abelian ; :: thesis: ( Image f is add-associative & Image f is right_zeroed & Image f is right_complementable )

now :: thesis: for u, v, w being Element of (Image f) holds (u + v) + w = u + (v + w)

let u, v, w be Element of (Image f); :: thesis: (u + v) + w = u + (v + w)
consider a being Element of R such that
A1: f . a = u by T6;
consider b being Element of R such that
A2: f . b = v by T6;
consider c being Element of R such that
A3: f . c = w by T6;
A4: v + w = (f . b) + (f . c) by A2, A3, T5;
u + v = (f . a) + (f . b) by A1, A2, T5;
hence (u + v) + w = ((f . a) + (f . b)) + (f . c) by A3, T5
.= (f . a) + ((f . b) + (f . c)) by RLVECT_1:def 3
.= u + (v + w) by A1, A4, T5 ;
:: thesis: verum

end;

hence Image f is add-associative ; :: thesis: ( Image f is right_zeroed & Image f is right_complementable )

now :: thesis: for v being Element of (Image f) holds v + (0. (Image f)) = v

let v be Element of (Image f); :: thesis: v + (0. (Image f)) = v
consider a being Element of R such that
A1: f . a = v by T6;
0. (Image f) = 0. S by defim;
then v + (0. (Image f)) = (f . a) + (0. S) by A1, T5
.= f . a ;
hence v + (0. (Image f)) = v by A1; :: thesis: verum

end;

hence Image f is right_zeroed ; :: thesis: Image f is right_complementable

now :: thesis: for x being Element of (Image f) holds x is right_complementable

let x be Element of (Image f); :: thesis: x is right_complementable
consider a being Element of R such that
A1: f . a = x by T6;
consider b being Element of R such that
A2: a + b = 0. R by ALGSTR_0:def 11;
dom f = the carrier of R by FUNCT_2:def 1;
then f . b in rng f by FUNCT_1:3;
then reconsider y = f . b as Element of (Image f) by defim;
0. (Image f) = 0. S by defim
.= f . (0. R) by hom1
.= (f . a) + (f . b) by A2, VECTSP_1:def 20
.= x + y by T5, A1 ;
hence x is right_complementable ; :: thesis: verum

end;

hence Image f is right_complementable ; :: thesis: verum