set W = Ker f;
set qf = CQFunctional f;
set qv = VectQuot V,(Ker f);
consider v being Vector of V such that
v <> 0. V and
A1: f . v <> 0. K by Th29;
reconsider cv = v + (Ker f) as Vector of (VectQuot V,(Ker f)) by Th24;
assume CQFunctional f is constant ; :: thesis: contradiction
then CQFunctional f = 0Functional (VectQuot V,(Ker f)) by Def7;
then 0. K = (CQFunctional f) . cv by HAHNBAN1:22
.= f . v by Th36 ;
hence contradiction by A1; :: thesis: verum