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