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))) & () . x1 = () . 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))) & () . xx1 = () . xx2 implies xx1 = xx2 )
assume AS: ( xx1 in the carrier of (VectQuot (V,(ker f))) & xx2 in the carrier of (VectQuot (V,(ker f))) & () . xx1 = () . 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 = () . x1 by
.= f . a2 by ;
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 ;
hence xx1 = xx2 by ; :: thesis: verum
end;
hence CQFunctional f is one-to-one by FUNCT_2:19; :: thesis: verum