set L = LKer f;
set vq = VectQuot (V,(LKer f));
set C = CosetSet (V,(LKer f));
set aC = addCoset (V,(LKer f));
set mC = lmultCoset (V,(LKer f));
defpred S₁[ set , set , set ] means for a being Vector of V st $1 = a + (LKer f) holds
$3 = f . (a,$2);

A1: now :: thesis: for A being Vector of (VectQuot (V,(LKer f)))
for w0 being Vector of W ex y being Element of the carrier of K st S₁[A,w0,y]

let A be Vector of (VectQuot (V,(LKer f))); :: thesis: for w0 being Vector of W ex y being Element of the carrier of K st S₁[A,w0,y]
let w0 be Vector of W; :: thesis: ex y being Element of the carrier of K st S₁[A,w0,y]
consider a being Vector of V such that
A2: A = a + (LKer f) by VECTSP10:22;
take y = f . (a,w0); :: thesis: S₁[A,w0,y]

now :: thesis: for a1 being Vector of V st A = a1 + (LKer f) holds
y = f . (a1,w0)

let a1 be Vector of V; :: thesis: ( A = a1 + (LKer f) implies y = f . (a1,w0) )
assume A = a1 + (LKer f) ; :: thesis: y = f . (a1,w0)
then a in a1 + (LKer f) by A2, VECTSP_4:44;
then consider w being Vector of V such that
A3: w in LKer f and
A4: a = a1 + w by VECTSP_4:42;
w in the carrier of (LKer f) by A3;
then w in leftker f by Def18;
then A5: ex aa being Vector of V st
( aa = w & ( for ww being Vector of W holds f . (aa,ww) = 0. K ) ) ;
thus y = (f . (a1,w0)) + (f . (w,w0)) by A4, Th26
.= (f . (a1,w0)) + (0. K) by A5
.= f . (a1,w0) by RLVECT_1:def 4 ; :: thesis: verum

end;

hence S₁[A,w0,y] ; :: thesis: verum

end;

consider ff being Function of [: the carrier of (VectQuot (V,(LKer f))), the carrier of W:], the carrier of K such that
A6: for A being Vector of (VectQuot (V,(LKer f)))
for w being Vector of W holds S₁[A,w,ff . (A,w)] from BINOP_1:sch 3(A1);
reconsider ff = ff as Form of (VectQuot (V,(LKer f))),W ;
A7: CosetSet (V,(LKer f)) = the carrier of (VectQuot (V,(LKer f))) by VECTSP10:def 6;

now :: thesis: for w being Vector of W holds FunctionalSAF (ff,w) is additive

let w be Vector of W; :: thesis: FunctionalSAF (ff,w) is additive
set ffw = FunctionalSAF (ff,w);

now :: thesis: for A, B being Vector of (VectQuot (V,(LKer f))) holds (FunctionalSAF (ff,w)) . (A + B) = ((FunctionalSAF (ff,w)) . A) + ((FunctionalSAF (ff,w)) . B)

let A, B be Vector of (VectQuot (V,(LKer f))); :: thesis: (FunctionalSAF (ff,w)) . (A + B) = ((FunctionalSAF (ff,w)) . A) + ((FunctionalSAF (ff,w)) . B)
consider a being Vector of V such that
A8: A = a + (LKer f) by VECTSP10:22;
consider b being Vector of V such that
A9: B = b + (LKer f) by VECTSP10:22;
A10: ( the addF of (VectQuot (V,(LKer f))) = addCoset (V,(LKer f)) & (addCoset (V,(LKer f))) . (A,B) = (a + b) + (LKer f) ) by A7, A8, A9, VECTSP10:def 3, VECTSP10:def 6;
thus (FunctionalSAF (ff,w)) . (A + B) = ff . ((A + B),w) by Th9
.= f . ((a + b),w) by A6, A10, RLVECT_1:2
.= (f . (a,w)) + (f . (b,w)) by Th26
.= (ff . (A,w)) + (f . (b,w)) by A6, A8
.= (ff . (A,w)) + (ff . (B,w)) by A6, A9
.= ((FunctionalSAF (ff,w)) . A) + (ff . (B,w)) by Th9
.= ((FunctionalSAF (ff,w)) . A) + ((FunctionalSAF (ff,w)) . B) by Th9 ; :: thesis: verum

end;

hence FunctionalSAF (ff,w) is additive ; :: thesis: verum

end;

then reconsider ff = ff as additiveSAF Form of (VectQuot (V,(LKer f))),W by Def12;

now :: thesis: for w being Vector of W holds FunctionalSAF (ff,w) is homogeneous

let w be Vector of W; :: thesis: FunctionalSAF (ff,w) is homogeneous
set ffw = FunctionalSAF (ff,w);

now :: thesis: for A being Vector of (VectQuot (V,(LKer f)))
for r being Element of K holds (FunctionalSAF (ff,w)) . (r * A) = r * ((FunctionalSAF (ff,w)) . A)

let A be Vector of (VectQuot (V,(LKer f))); :: thesis: for r being Element of K holds (FunctionalSAF (ff,w)) . (r * A) = r * ((FunctionalSAF (ff,w)) . A)
let r be Element of K; :: thesis: (FunctionalSAF (ff,w)) . (r * A) = r * ((FunctionalSAF (ff,w)) . A)
consider a being Vector of V such that
A11: A = a + (LKer f) by VECTSP10:22;
A12: ( the lmult of (VectQuot (V,(LKer f))) = lmultCoset (V,(LKer f)) & (lmultCoset (V,(LKer f))) . (r,A) = (r * a) + (LKer f) ) by A7, A11, VECTSP10:def 5, VECTSP10:def 6;
thus (FunctionalSAF (ff,w)) . (r * A) = ff . ((r * A),w) by Th9
.= f . ((r * a),w) by A6, A12
.= r * (f . (a,w)) by Th31
.= r * (ff . (A,w)) by A6, A11
.= r * ((FunctionalSAF (ff,w)) . A) by Th9 ; :: thesis: verum

end;

hence FunctionalSAF (ff,w) is homogeneous ; :: thesis: verum

end;

then reconsider ff = ff as additiveSAF homogeneousSAF Form of (VectQuot (V,(LKer f))),W by Def14;
take ff ; :: thesis: for A being Vector of (VectQuot (V,(LKer f)))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
ff . (A,w) = f . (v,w)
thus for A being Vector of (VectQuot (V,(LKer f)))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
ff . (A,w) = f . (v,w) by A6; :: thesis: verum