set W = Ker (f *' );
set qf = QcFunctional f;
set qv = VectQuot V,(Ker (f *' ));
assume QcFunctional f is constant ; :: thesis: contradiction
then A1: QcFunctional f = 0Functional (VectQuot V,(Ker (f *' ))) by VECTSP10:def 7;
consider v being Vector of V such that
A2: ( v <> 0. V & f . v <> 0. F_Complex ) by VECTSP10:29;
reconsider cv = v + (Ker (f *' )) as Vector of (VectQuot V,(Ker (f *' ))) by VECTSP10:24;
0. F_Complex = (QcFunctional f) . cv by A1, HAHNBAN1:22
.= f . v by Th29 ;
hence contradiction by A2; :: thesis: verum