now let x,
y be
Element of
K;
for v, w being Element of (V *') holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. K) * v = v )let v,
w be
Element of
(V *');
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. K) * v = v )reconsider f =
v,
g =
w as
linear-Functional of
V by Def14;
thus x * (v + w) =
the
lmult of
(V *') . (
x,
(f + g))
by Def14
.=
x * (f + g)
by Def14
.=
(x * f) + (x * g)
by Th25
.=
the
addF of
(V *') . (
(x * f),
(x * g))
by Def14
.=
the
addF of
(V *') . (
( the lmult of (V *') . (x,f)),
(x * g))
by Def14
.=
(x * v) + (x * w)
by Def14
;
( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. K) * v = v )thus (x + y) * v =
(x + y) * f
by Def14
.=
(x * f) + (y * f)
by Th26
.=
the
addF of
(V *') . (
(x * f),
(y * f))
by Def14
.=
the
addF of
(V *') . (
( the lmult of (V *') . (x,f)),
(y * f))
by Def14
.=
(x * v) + (y * v)
by Def14
;
( (x * y) * v = x * (y * v) & (1. K) * v = v )thus (x * y) * v =
(x * y) * f
by Def14
.=
x * (y * f)
by Th27
.=
the
lmult of
(V *') . (
x,
(y * f))
by Def14
.=
x * (y * v)
by Def14
;
(1. K) * v = vthus (1. K) * v =
(1. K) * f
by Def14
.=
v
by Th28
;
verum end;
hence
( V *' is vector-distributive & V *' is scalar-distributive & V *' is scalar-associative & V *' is scalar-unital )
by VECTSP_1:def 26, VECTSP_1:def 27, VECTSP_1:def 28, VECTSP_1:def 29; verum