set T = CQFunctional f;
set Vq = VectQuot (V,(ker f));
for x1, x2 being object st x1 in the carrier of (VectQuot (V,(ker f))) & x2 in the carrier of (VectQuot (V,(ker f))) & (CQFunctional f) . x1 = (CQFunctional f) . x2 holds
x1 = x2

proof

let xx1, xx2 be object ; :: thesis: ( xx1 in the carrier of (VectQuot (V,(ker f))) & xx2 in the carrier of (VectQuot (V,(ker f))) & (CQFunctional f) . xx1 = (CQFunctional f) . xx2 implies xx1 = xx2 )
assume AS: ( xx1 in the carrier of (VectQuot (V,(ker f))) & xx2 in the carrier of (VectQuot (V,(ker f))) & (CQFunctional f) . xx1 = (CQFunctional f) . xx2 ) ; :: thesis: xx1 = xx2
then reconsider x1 = xx1, x2 = xx2 as Vector of (VectQuot (V,(ker f))) ;
consider a1 being Vector of V such that
A14: x1 = a1 + (ker f) by VECTSP10:22;
consider a2 being Vector of V such that
A15: x2 = a2 + (ker f) by VECTSP10:22;
f . a1 = (CQFunctional f) . x1 by A14, Def12
.= f . a2 by AS, A15, Def12 ;
then A16: a1 - a2 in ker f by RANKNULL:17;
a1 = a1 - (0. V)
.= a1 - (a2 - a2) by VECTSP_1:19
.= a2 + (a1 - a2) by RLVECT_1:29 ;
then ( a1 in x1 & a1 in x2 ) by A14, A15, A16, VECTSP_4:44;
hence xx1 = xx2 by VECTSP_4:56, A14, A15; :: thesis: verum

end;

hence CQFunctional f is one-to-one by FUNCT_2:19; :: thesis: verum