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

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

hence
CQFunctional f is one-to-one
by FUNCT_2:19; :: thesis: verum
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;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