V is_the_direct_sum_of W, Lin {v} by VECTSP_5:def 5;
then A2: ( VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #) = W + (Lin {v}) & W /\ (Lin {v}) = (0). V ) by VECTSP_5:def 4;
then reconsider y = v as Vector of (W + (Lin {v})) ;

now

assume v in W ; :: thesis: contradiction
then A3: v in the carrier of W by STRUCT_0:def 5;
v in {v} by TARSKI:def 1;
then v in Lin {v} by VECTSP_7:13;
then v in the carrier of (Lin {v}) by STRUCT_0:def 5;
then v in the carrier of W /\ the carrier of (Lin {v}) by A3, XBOOLE_0:def 4;
then v in the carrier of (W /\ (Lin {v})) by VECTSP_5:def 2;
then v in {(0. V)} by A2, VECTSP_4:def 3;
hence contradiction by A1, TARSKI:def 1; :: thesis: verum

end;

then consider psi being linear-Functional of (W + (Lin {v})) such that
A4: ( psi | the carrier of W = 0Functional W & psi . y = 1_ K ) by Th28;
reconsider f = psi as Functional of V by A2;
A5: f is additive

proof

let v1, v2 be Vector of V; :: according to HAHNBAN1:def 11 :: thesis: f . (v1 + v2) = (f . v1) + (f . v2)
reconsider w1 = v1, w2 = v2 as Vector of (W + (Lin {v})) by A2;
v1 + v2 = w1 + w2 by A2;
hence f . (v1 + v2) = (f . v1) + (f . v2) by HAHNBAN1:def 11; :: thesis: verum

end;

f is homogeneous

proof

let v1 be Vector of V; :: according to HAHNBAN1:def 12 :: thesis: for b₁ being Element of the carrier of K holds f . (b₁ * v1) = b₁ * (f . v1)
let a be Element of K; :: thesis: f . (a * v1) = a * (f . v1)
reconsider w1 = v1 as Vector of (W + (Lin {v})) by A2;
a * v1 = the lmult of (W + (Lin {v})) . a,w1 by A2, VECTSP_1:def 24
.= a * w1 by VECTSP_1:def 24 ;
hence f . (a * v1) = a * (f . v1) by HAHNBAN1:def 12; :: thesis: verum

end;

then reconsider f = f as linear-Functional of V by A5;
A6: not f is constant

proof

assume A7: f is constant ; :: thesis: contradiction
A8: the carrier of V = dom f by FUNCT_2:def 1;
f . (0. V) = 0. K by HAHNBAN1:def 13;
hence contradiction by A4, A7, A8, FUNCT_1:def 16; :: thesis: verum

end;

reconsider f = f as V8() non trivial linear-Functional of V by A6;
take f ; :: thesis: ( f . v = 1_ K & f | the carrier of W = 0Functional W )
thus ( f . v = 1_ K & f | the carrier of W = 0Functional W ) by A4; :: thesis: verum