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 Th28;
reconsider cv = v + (Ker f) as Vector of (VectQuot (V,(Ker f))) by Th23;
assume CQFunctional f is constant ; :: thesis: contradiction
then CQFunctional f = 0Functional (VectQuot (V,(Ker f))) ;
then 0. K = (CQFunctional f) . cv by HAHNBAN1:14
.= f . v by Th35 ;
hence contradiction by A1; :: thesis: verum