set I = Image f;
hence
Image f is associative
; ( Image f is well-unital & Image f is distributive )
hence
Image f is well-unital
; Image f is distributive
now for u, v, w being Element of (Image f) holds
( u * (v + w) = (u * v) + (u * w) & (v + w) * u = (v * u) + (w * u) )let u,
v,
w be
Element of
(Image f);
( u * (v + w) = (u * v) + (u * w) & (v + w) * u = (v * u) + (w * u) )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;
A5:
u * v = (f . a) * (f . b)
by A1, A2, T5;
A6:
u * w = (f . a) * (f . c)
by A1, A3, T5;
thus u * (v + w) =
(f . a) * ((f . b) + (f . c))
by A1, A4, T5
.=
((f . a) * (f . b)) + ((f . a) * (f . c))
by VECTSP_1:def 7
.=
(u * v) + (u * w)
by A5, A6, T5
;
(v + w) * u = (v * u) + (w * u)A7:
v * u = (f . b) * (f . a)
by A1, A2, T5;
A8:
w * u = (f . c) * (f . a)
by A1, A3, T5;
thus (v + w) * u =
((f . b) + (f . c)) * (f . a)
by A1, A4, T5
.=
((f . b) * (f . a)) + ((f . c) * (f . a))
by VECTSP_1:def 7
.=
(v * u) + (w * u)
by A7, A8, T5
;
verum end;
hence
Image f is distributive
; verum