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