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

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

let u, v be Element of (Image_hom_Ext_eval (x,F)); :: thesis: u * v = v * u
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;
thus u * v = ((hom_Ext_eval (x,F)) . a) * ((hom_Ext_eval (x,F)) . b) by A1, A2, T5
.= ((hom_Ext_eval (x,F)) . b) * ((hom_Ext_eval (x,F)) . a) by GROUP_1:def 12
.= v * u by A1, A2, T5 ; :: thesis: verum

end;

hence Image_hom_Ext_eval (x,F) is commutative ; :: thesis: ( Image_hom_Ext_eval (x,F) is associative & Image_hom_Ext_eval (x,F) is well-unital & Image_hom_Ext_eval (x,F) is distributive )

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 GROUP_1:def 3
.= u * (v * w) by A1, A4, T5 ;
:: thesis: verum

end;

hence Image_hom_Ext_eval (x,F) is associative ; :: thesis: ( Image_hom_Ext_eval (x,F) is well-unital & Image_hom_Ext_eval (x,F) is distributive )

now :: thesis: for x being Element of (Image_hom_Ext_eval (x,F)) holds
( x * (1. (Image_hom_Ext_eval (x,F))) = x & (1. (Image_hom_Ext_eval (x,F))) * x = x )

let x be Element of (Image_hom_Ext_eval (x,F)); :: thesis: ( x * (1. (Image_hom_Ext_eval (x,F))) = x & (1. (Image_hom_Ext_eval (x,F))) * x = x )
consider a being Element of (Polynom-Ring (n,F)) such that
A1: (hom_Ext_eval (x,F)) . a = x by T6;
A2: 1. E = 1. (Image_hom_Ext_eval (x,F)) by defIm;
thus x * (1. (Image_hom_Ext_eval (x,F))) = ((hom_Ext_eval (x,F)) . a) * (1. E) by A1, A2, T5
.= x by A1 ; :: thesis: (1. (Image_hom_Ext_eval (x,F))) * x = x
thus (1. (Image_hom_Ext_eval (x,F))) * x = (1. E) * ((hom_Ext_eval (x,F)) . a) by A1, A2, T5
.= x by A1 ; :: thesis: verum

end;

hence Image_hom_Ext_eval (x,F) is well-unital ; :: thesis: Image_hom_Ext_eval (x,F) is distributive

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

let u, v, w be Element of (Image_hom_Ext_eval (x,F)); :: thesis: ( u * (v + w) = (u * v) + (u * w) & (v + w) * u = (v * u) + (w * u) )
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;
A5: u * v = ((hom_Ext_eval (x,F)) . a) * ((hom_Ext_eval (x,F)) . b) by A1, A2, T5;
A6: u * w = ((hom_Ext_eval (x,F)) . a) * ((hom_Ext_eval (x,F)) . c) by A1, A3, T5;
thus u * (v + w) = ((hom_Ext_eval (x,F)) . a) * (((hom_Ext_eval (x,F)) . b) + ((hom_Ext_eval (x,F)) . c)) by A1, A4, T5
.= (((hom_Ext_eval (x,F)) . a) * ((hom_Ext_eval (x,F)) . b)) + (((hom_Ext_eval (x,F)) . a) * ((hom_Ext_eval (x,F)) . c)) by VECTSP_1:def 7
.= (u * v) + (u * w) by A5, A6, T5 ; :: thesis: (v + w) * u = (v * u) + (w * u)
A7: v * u = ((hom_Ext_eval (x,F)) . b) * ((hom_Ext_eval (x,F)) . a) by A1, A2, T5;
A8: w * u = ((hom_Ext_eval (x,F)) . c) * ((hom_Ext_eval (x,F)) . a) by A1, A3, T5;
thus (v + w) * u = (((hom_Ext_eval (x,F)) . b) + ((hom_Ext_eval (x,F)) . c)) * ((hom_Ext_eval (x,F)) . a) by A1, A4, T5
.= (((hom_Ext_eval (x,F)) . b) * ((hom_Ext_eval (x,F)) . a)) + (((hom_Ext_eval (x,F)) . c) * ((hom_Ext_eval (x,F)) . a)) by VECTSP_1:def 7
.= (v * u) + (w * u) by A7, A8, T5 ; :: thesis: verum

end;

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