consider v being Vector of V such that
A1: v <> 0. V by STRUCT_0:def 18;
set W = the Linear_Compl of Lin {v};
A2: V is_the_direct_sum_of the Linear_Compl of Lin {v}, 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 #) = the Linear_Compl of Lin {v} + (Lin {v}) ;
then reconsider y = v as Vector of ( the Linear_Compl of Lin {v} + (Lin {v})) ;
A4: the Linear_Compl of Lin {v} /\ (Lin {v}) = (0). V by A2;
now :: thesis: not v in the Linear_Compl of Lin {v}
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 the Linear_Compl of Lin {v} ; :: thesis: contradiction
then v in the carrier of the Linear_Compl of Lin {v} ;
then v in the carrier of the Linear_Compl of Lin {v} /\ the carrier of (Lin {v}) by A5, XBOOLE_0:def 4;
then v in the carrier of ( the Linear_Compl of Lin {v} /\ (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 ( the Linear_Compl of Lin {v} + (Lin {v})) such that
psi | the carrier of the Linear_Compl of Lin {v} = 0Functional the Linear_Compl of Lin {v} and
A6: psi . y = 1_ K by Th27;
reconsider f = psi as Functional of V by A3;
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 VECTSP_1:def 19 :: thesis: f . (v1 + v2) = (f . v1) + (f . v2)
reconsider w1 = v1, w2 = v2 as Vector of ( the Linear_Compl of Lin {v} + (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;
thus f is homogeneous :: thesis: ( not f is constant & not f is trivial )
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 ( the Linear_Compl of Lin {v} + (Lin {v})) by A3;
a * v1 = the lmult of ( the Linear_Compl of Lin {v} + (Lin {v})) . (a,w1) by A3
.= a * w1 ;
hence f . (a * v1) = a * (f . v1) by HAHNBAN1:def 8; :: thesis: verum
end;
then reconsider f1 = f as homogeneous Functional of V ;
thus not f is constant :: thesis: not f is trivial
proof
A7: ( the carrier of V = dom f & f1 . (0. V) = 0. K ) by FUNCT_2:def 1, HAHNBAN1:def 9;
assume f is constant ; :: thesis: contradiction
hence contradiction by A6, A7; :: thesis: verum
end;
thus not f is trivial :: thesis: verum
proof
set x = [v,(1_ K)];
set y = [(0. V),(0. K)];
A8: the carrier of V = dom f by FUNCT_2:def 1;
then A9: [v,(1_ K)] in f by A6, FUNCT_1:1;
f1 . (0. V) = 0. K by HAHNBAN1:def 9;
then A10: [(0. V),(0. K)] in f by A8, FUNCT_1:1;
assume A11: f is trivial ; :: thesis: contradiction
per cases ( f = {} or ex z being object st f = {z} ) by A11, ZFMISC_1:131;
suppose ex z being object st f = {z} ; :: thesis: contradiction
then consider z being object such that
A12: f = {z} ;
( z = [v,(1_ K)] & z = [(0. V),(0. K)] ) by A9, A10, A12, TARSKI:def 1;
hence contradiction by XTUPLE_0:1; :: thesis: verum
end;
end;
end;