let x, y be Element of K; :: according to VECTSP_1:def 26 :: thesis: for b₁, b₂ being Element of the carrier of (V *' ) holds
( x * (b₁ + b₂) = (x * b₁) + (x * b₂) & (x + y) * b₁ = (x * b₁) + (y * b₁) & (x * y) * b₁ = x * (y * b₁) & (1. K) * b₁ = b₁ )
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 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 ; :: 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 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 ; :: thesis: ( (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 ; :: thesis: (1. K) * v = v
thus (1. K) * v = (1. K) * f by Def14
.= v by Th28 ; :: thesis: verum