consider v being Vector of V such that
A1: v <> 0. V by STRUCT_0:def 19;
consider W being Linear_Compl of Lin {v};
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;
take f ; :: thesis: ( f is additive & f is homogeneous & not f is constant & not f is trivial )
thus f is additive :: thesis: ( f is homogeneous & not f is constant & not f is trivial )

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;

thus f is homogeneous :: thesis: ( not f is constant & not f is trivial )

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 f1 = f as homogeneous Functional of V ;
thus not f is constant :: thesis: not f is trivial

proof

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

end;

thus not f is trivial :: thesis: verum

proof

set x = [v,(1_ K)];
set y = [(0. V),(0. K)];
assume A7: f is trivial ; :: thesis: contradiction
A8: the carrier of V = dom f by FUNCT_2:def 1;
f1 . (0. V) = 0. K by HAHNBAN1:def 13;
then A9: ( [v,(1_ K)] in f & [(0. V),(0. K)] in f ) by A4, A8, FUNCT_1:8;

per cases ( f = {} or ex z being set st f = {z} ) by A7, REALSET1:def 4;

suppose f = {} ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

suppose ex z being set st f = {z} ; :: thesis: contradiction

then consider z being set such that
A10: f = {z} ;
( z = [v,(1_ K)] & z = [(0. V),(0. K)] ) by A9, A10, TARSKI:def 1;
hence contradiction by ZFMISC_1:33; :: thesis: verum

end;

end;

end;