now :: thesis: 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; :: thesis: 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 *'); :: thesis: ( 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 ; :: thesis: ( (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 ; :: thesis: ( (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 ; :: thesis: (1. K) * v = v
thus (1. K) * v = (1. K) * f by Def10
.= v by Th18 ; :: thesis: verum

end;

hence ( V *' is vector-distributive & V *' is scalar-distributive & V *' is scalar-associative & V *' is scalar-unital ) ; :: thesis: verum