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);
A2: now :: thesis: for A being Vector of (VectQuot (V,W)) ex y being Element of the carrier of K st S1[A,y]
let A be Vector of (VectQuot (V,W)); :: thesis: ex y being Element of the carrier of K st S1[A,y]
consider a being Vector of V such that
A3: A = a + W by Th22;
take y = f . a; :: thesis: S1[A,y]
thus S1[A,y] :: thesis: verum
proof
let a1 be Vector of V; :: thesis: ( A = a1 + W implies y = f . a1 )
assume A = a1 + W ; :: thesis: y = f . a1
then a in a1 + W by A3, VECTSP_4:44;
then consider w being Vector of V such that
A4: w in W and
A5: a = a1 + w by VECTSP_4:42;
w in the carrier of W by A4;
then w in ker f by A1;
then A6: ex aa being Vector of V st
( aa = w & f . aa = 0. K ) ;
thus y = (f . a1) + (f . w) by A5, VECTSP_1:def 20
.= f . a1 by A6, RLVECT_1:def 4 ; :: thesis: verum
end;
end;
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 :: thesis: 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)); :: thesis: 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 ;
:: thesis: verum
end;
then reconsider ff = ff as additive Functional of (VectQuot (V,W)) by VECTSP_1:def 20;
take ff ; :: thesis: 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; :: thesis: verum