defpred S1[ set , set ] means for a being Vector of V st $1 = a + W holds
$2 = f . a;
set aC = addCoset (V,W);
set C = CosetSet (V,W);
set vq = VectQuot (V,W);
consider ff being Function of the carrier of (VectQuot (V,W)), the carrier of K such that
A7:
for A being Vector of (VectQuot (V,W)) holds S1[A,ff . A]
from FUNCT_2:sch 3(A2);
reconsider ff = ff as Functional of (VectQuot (V,W)) ;
A8:
CosetSet (V,W) = the carrier of (VectQuot (V,W))
by Def6;
now for A, B being Vector of (VectQuot (V,W)) holds ff . (A + B) = (ff . A) + (ff . B)A9:
the
addF of
(VectQuot (V,W)) = addCoset (
V,
W)
by Def6;
let A,
B be
Vector of
(VectQuot (V,W));
ff . (A + B) = (ff . A) + (ff . B)consider a being
Vector of
V such that A10:
A = a + W
by Th22;
consider b being
Vector of
V such that A11:
B = b + W
by Th22;
(addCoset (V,W)) . (
A,
B)
= (a + b) + W
by A8, A10, A11, Def3;
hence ff . (A + B) =
f . (a + b)
by A7, A9
.=
(f . a) + (f . b)
by VECTSP_1:def 20
.=
(ff . A) + (f . b)
by A7, A10
.=
(ff . A) + (ff . B)
by A7, A11
;
verum end;
then reconsider ff = ff as additive Functional of (VectQuot (V,W)) by VECTSP_1:def 20;
take
ff
; for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
ff . A = f . a
thus
for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
ff . A = f . a
by A7; verum