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