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