now for x, y being 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 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 Def10;
thus x * (v + w) =
the
lmult of
(V *') . (
x,
(f + g))
by Def10
.=
x * (f + g)
by Def10
.=
(x * f) + (x * g)
by Th15
.=
the
addF of
(V *') . (
(x * f),
(x * g))
by Def10
.=
the
addF of
(V *') . (
( the lmult of (V *') . (x,f)),
(x * g))
by Def10
.=
(x * v) + (x * w)
by Def10
;
( (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 Def10
.=
(x * f) + (y * f)
by Th16
.=
the
addF of
(V *') . (
(x * f),
(y * f))
by Def10
.=
the
addF of
(V *') . (
( the lmult of (V *') . (x,f)),
(y * f))
by Def10
.=
(x * v) + (y * v)
by Def10
;
( (x * y) * v = x * (y * v) & (1. K) * v = v )thus (x * y) * v =
(x * y) * f
by Def10
.=
x * (y * f)
by Th17
.=
the
lmult of
(V *') . (
x,
(y * f))
by Def10
.=
x * (y * v)
by Def10
;
(1. K) * v = vthus (1. K) * v =
(1. K) * f
by Def10
.=
v
by Th18
;
verum end;
hence
( V *' is vector-distributive & V *' is scalar-distributive & V *' is scalar-associative & V *' is scalar-unital )
; verum