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:28;
reconsider cv = v + (Ker (f *')) as Vector of (VectQuot (V,(Ker (f *')))) by VECTSP10:23;
assume QcFunctional f is V23() ; :: thesis: contradiction
then QcFunctional f = 0Functional (VectQuot (V,(Ker (f *')))) ;
then 0. F_Complex = (QcFunctional f) . cv by HAHNBAN1:14
.= f . v by Th26 ;
hence contradiction by A1; :: thesis: verum