defpred S₁[ 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

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
A3: 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 A3, VECTSP_4:59;
then consider w being Vector of V such that
A4: w in W and
A5: a = a1 + w by VECTSP_4:57;
w in the carrier of W by A4, STRUCT_0:def 5;
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, 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(A2);
reconsider ff = ff as Functional of (VectQuot V,W) ;
A8: CosetSet V,W = the carrier of (VectQuot V,W) by Def6;

now

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 Th23;
consider b being Vector of V such that
A11: B = b + W by Th23;
(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 HAHNBAN1:def 11
.= (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 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