set vq = VectQuot V,W;
set C = CosetSet V,W;
set aC = addCoset V,W;
A2: CosetSet V,W = the carrier of (VectQuot V,W) by Def6;
defpred S₁[ set , set ] means for a being Vector of V st $1 = a + W holds
$2 = f . a;

A3: now

let A be Vector of (VectQuot V,W); :: thesis: ex y being Element of the carrier of K st S₁[A,y]
consider a being Vector of V such that
A4: A = a + W by Th23;
take y = f . a; :: thesis: S₁[A,y]
thus S₁[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 A4, VECTSP_4:59;
then consider w being Vector of V such that
A5: ( w in W & a = a1 + w ) by VECTSP_4:57;
w in the carrier of W by A5, STRUCT_0:def 5;
then w in ker f by A1;
then consider aa being Vector of V such that
A6: ( aa = w & f . aa = 0. K ) ;
thus y = (f . a1) + (f . w) by A5, HAHNBAN1:def 11
.= f . a1 by A6, RLVECT_1:def 7 ; :: 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 S₁[A,ff . A] from FUNCT_2:sch 3(A3);
reconsider ff = ff as Functional of (VectQuot V,W) ;

now

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
A8: A = a + W by Th23;
consider b being Vector of V such that
A9: B = b + W by Th23;
A10: the addF of (VectQuot V,W) = addCoset V,W by Def6;
(addCoset V,W) . A,B = (a + b) + W by A2, A8, A9, Def3;
hence ff . (A + B) = f . (a + b) by A7, A10
.= (f . a) + (f . b) by HAHNBAN1:def 11
.= (ff . A) + (f . b) by A7, A8
.= (ff . A) + (ff . B) by A7, A9 ;
:: thesis: verum

end;

then reconsider ff = ff as additive Functional of (VectQuot V,W) by HAHNBAN1:def 11;
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