A2: V is_the_direct_sum_of W, Lin {v} by VECTSP_5:def 5;
then A3: ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = W + (Lin {v}) ;
then reconsider y = v as Vector of (W + (Lin {v})) ;
A4: W /\ (Lin {v}) = (0). V by A2;
now :: thesis: not v in W
v in {v} by TARSKI:def 1;
then v in Lin {v} by VECTSP_7:8;
then A5: v in the carrier of (Lin {v}) ;
assume v in W ; :: thesis: contradiction
then v in the carrier of W ;
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 Th27;
reconsider f = psi as Functional of V by A3;
A8: f is additive
proof
let v1, v2 be Vector of V; :: according to VECTSP_1:def 19 :: 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 VECTSP_1:def 20; :: thesis: verum
end;
f is homogeneous
proof
let v1 be Vector of V; :: according to HAHNBAN1:def 8 :: thesis: for b1 being Element of the carrier of K holds f . (b1 * v1) = b1 * (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
.= a * w1 ;
hence f . (a * v1) = a * (f . v1) by HAHNBAN1:def 8; :: thesis: verum
end;
then reconsider f = f as linear-Functional of V by A8;
f is V8()
proof
A9: ( the carrier of V = dom f & f . (0. V) = 0. K ) by FUNCT_2:def 1, HAHNBAN1:def 9;
assume f is V8() ; :: thesis: contradiction
hence contradiction by A7, A9; :: 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