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

now

v in {v} by TARSKI:def 1;
then v in Lin {v} by VECTSP_7:13;
then A5: v in the carrier of (Lin {v}) by STRUCT_0:def 5;
assume v in W ; :: thesis: contradiction
then v in the carrier of W by STRUCT_0:def 5;
then v in the carrier of W /\ the carrier of (Lin {v}) by A5, XBOOLE_0:def 4;
then v in the carrier of (W /\ (Lin {v})) by VECTSP_5:def 2;
then v in {(0. V)} by A4, 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
A6: psi | the carrier of W = 0Functional W and
A7: psi . y = 1_ K by Th28;
reconsider f = psi as Functional of V by A3;
A8: f is additive

proof

let v1, v2 be Vector of V; :: according to GRCAT_1:def 13 :: thesis: f . (v1 + v2) = (f . v1) + (f . v2)
reconsider w1 = v1, w2 = v2 as Vector of (W + (Lin {v})) by A3;
v1 + v2 = w1 + w2 by A3;
hence f . (v1 + v2) = (f . v1) + (f . v2) by GRCAT_1:def 13; :: 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 A3;
a * v1 = the lmult of (W + (Lin {v})) . a,w1 by A3, 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 A8;
not f is constant

proof

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

end;

then reconsider f = f as V8() non trivial linear-Functional of V ;
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 A6, A7; :: thesis: verum