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