set I = Image_hom_Ext_eval (x,F);
set f = hom_Ext_eval (x,F);
set R = Polynom-Ring (n,F);

now :: thesis: for v, w being Element of (Image_hom_Ext_eval (x,F)) holds v + w = w + v

let v, w be Element of (Image_hom_Ext_eval (x,F)); :: thesis: v + w = w + v
consider a being Element of (Polynom-Ring (n,F)) such that
A1: (hom_Ext_eval (x,F)) . a = v by T6;
consider b being Element of (Polynom-Ring (n,F)) such that
A2: (hom_Ext_eval (x,F)) . b = w by T6;
thus v + w = ((hom_Ext_eval (x,F)) . a) + ((hom_Ext_eval (x,F)) . b) by A1, A2, T5
.= w + v by A1, A2, T5 ; :: thesis: verum

end;

hence Image_hom_Ext_eval (x,F) is Abelian ; :: thesis: ( Image_hom_Ext_eval (x,F) is add-associative & Image_hom_Ext_eval (x,F) is right_zeroed & Image_hom_Ext_eval (x,F) is right_complementable )

now :: thesis: for u, v, w being Element of (Image_hom_Ext_eval (x,F)) holds (u + v) + w = u + (v + w)

let u, v, w be Element of (Image_hom_Ext_eval (x,F)); :: thesis: (u + v) + w = u + (v + w)
consider a being Element of (Polynom-Ring (n,F)) such that
A1: (hom_Ext_eval (x,F)) . a = u by T6;
consider b being Element of (Polynom-Ring (n,F)) such that
A2: (hom_Ext_eval (x,F)) . b = v by T6;
consider c being Element of (Polynom-Ring (n,F)) such that
A3: (hom_Ext_eval (x,F)) . c = w by T6;
A4: v + w = ((hom_Ext_eval (x,F)) . b) + ((hom_Ext_eval (x,F)) . c) by A2, A3, T5;
u + v = ((hom_Ext_eval (x,F)) . a) + ((hom_Ext_eval (x,F)) . b) by A1, A2, T5;
hence (u + v) + w = (((hom_Ext_eval (x,F)) . a) + ((hom_Ext_eval (x,F)) . b)) + ((hom_Ext_eval (x,F)) . c) by A3, T5
.= ((hom_Ext_eval (x,F)) . a) + (((hom_Ext_eval (x,F)) . b) + ((hom_Ext_eval (x,F)) . c)) by RLVECT_1:def 3
.= u + (v + w) by A1, A4, T5 ;
:: thesis: verum

end;

hence Image_hom_Ext_eval (x,F) is add-associative ; :: thesis: ( Image_hom_Ext_eval (x,F) is right_zeroed & Image_hom_Ext_eval (x,F) is right_complementable )

now :: thesis: for v being Element of (Image_hom_Ext_eval (x,F)) holds v + (0. (Image_hom_Ext_eval (x,F))) = v

let v be Element of (Image_hom_Ext_eval (x,F)); :: thesis: v + (0. (Image_hom_Ext_eval (x,F))) = v
consider a being Element of (Polynom-Ring (n,F)) such that
A1: (hom_Ext_eval (x,F)) . a = v by T6;
0. (Image_hom_Ext_eval (x,F)) = 0. E by defIm;
then v + (0. (Image_hom_Ext_eval (x,F))) = ((hom_Ext_eval (x,F)) . a) + (0. E) by A1, T5
.= (hom_Ext_eval (x,F)) . a ;
hence v + (0. (Image_hom_Ext_eval (x,F))) = v by A1; :: thesis: verum

end;

hence Image_hom_Ext_eval (x,F) is right_zeroed ; :: thesis: Image_hom_Ext_eval (x,F) is right_complementable

now :: thesis: for x being Element of (Image_hom_Ext_eval (x,F)) holds x is right_complementable

let x be Element of (Image_hom_Ext_eval (x,F)); :: thesis: x is right_complementable
consider a being Element of (Polynom-Ring (n,F)) such that
A1: (hom_Ext_eval (x,F)) . a = x by T6;
consider b being Element of (Polynom-Ring (n,F)) such that
A2: a + b = 0. (Polynom-Ring (n,F)) by ALGSTR_0:def 11;
dom (hom_Ext_eval (x,F)) = the carrier of (Polynom-Ring (n,F)) by FUNCT_2:def 1;
then (hom_Ext_eval (x,F)) . b in rng (hom_Ext_eval (x,F)) by FUNCT_1:3;
then reconsider y = (hom_Ext_eval (x,F)) . b as Element of (Image_hom_Ext_eval (x,F)) by defIm;
0. (Image_hom_Ext_eval (x,F)) = 0. E by defIm
.= (hom_Ext_eval (x,F)) . (0. (Polynom-Ring (n,F))) by RING_2:6
.= ((hom_Ext_eval (x,F)) . a) + ((hom_Ext_eval (x,F)) . b) by A2, VECTSP_1:def 20
.= x + y by T5, A1 ;
hence x is right_complementable ; :: thesis: verum

end;

hence Image_hom_Ext_eval (x,F) is right_complementable ; :: thesis: verum