assume A1: V *' is trivial ; :: thesis: contradiction
consider g being V8() linear-Functional of V;
A2: g <> 0Functional V ;
reconsider g = g as Element of (V *' ) by HAHNBAN1:def 14;
g = 0. (V *' ) by A1, STRUCT_0:def 19;
hence contradiction by A2, HAHNBAN1:def 14; :: thesis: verum