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