set L = LKer f;
set vq = VectQuot (V,(LKer f));
set Cv = CosetSet (V,(LKer f));
set aCv = addCoset (V,(LKer f));
set mCv = lmultCoset (V,(LKer f));
set R = RKer f;
set wq = VectQuot (W,(RKer f));
set Cw = CosetSet (W,(RKer f));
set aCw = addCoset (W,(RKer f));
set mCw = lmultCoset (W,(RKer f));
defpred S₁[ set , set , set ] means for v being Vector of V
for w being Vector of W st $1 = v + (LKer f) & $2 = w + (RKer f) holds
$3 = f . (v,w);

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

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

now :: thesis: for a1 being Vector of V
for b1 being Vector of W st A = a1 + (LKer f) & B = b1 + (RKer f) holds
y = f . (a1,b1)

let a1 be Vector of V; :: thesis: for b1 being Vector of W st A = a1 + (LKer f) & B = b1 + (RKer f) holds
y = f . (a1,b1)
let b1 be Vector of W; :: thesis: ( A = a1 + (LKer f) & B = b1 + (RKer f) implies y = f . (a1,b1) )
assume A = a1 + (LKer f) ; :: thesis: ( B = b1 + (RKer f) implies y = f . (a1,b1) )
then a in a1 + (LKer f) by A2, VECTSP_4:44;
then consider vv being Vector of V such that
A4: vv in LKer f and
A5: a = a1 + vv by VECTSP_4:42;
vv in the carrier of (LKer f) by A4;
then vv in leftker f by Def18;
then A6: ex aa being Vector of V st
( aa = vv & ( for w0 being Vector of W holds f . (aa,w0) = 0. K ) ) ;
assume B = b1 + (RKer f) ; :: thesis: y = f . (a1,b1)
then b in b1 + (RKer f) by A3, VECTSP_4:44;
then consider ww being Vector of W such that
A7: ww in RKer f and
A8: b = b1 + ww by VECTSP_4:42;
ww in the carrier of (RKer f) by A7;
then ww in rightker f by Def19;
then A9: ex bb being Vector of W st
( bb = ww & ( for v0 being Vector of V holds f . (v0,bb) = 0. K ) ) ;
thus y = ((f . (a1,b1)) + (f . (a1,ww))) + ((f . (vv,b1)) + (f . (vv,ww))) by A5, A8, Th28
.= ((f . (a1,b1)) + (0. K)) + ((f . (vv,b1)) + (f . (vv,ww))) by A9
.= ((f . (a1,b1)) + (0. K)) + ((0. K) + (f . (vv,ww))) by A6
.= (f . (a1,b1)) + ((0. K) + (f . (vv,ww))) by RLVECT_1:def 4
.= (f . (a1,b1)) + (f . (vv,ww)) by RLVECT_1:4
.= (f . (a1,b1)) + (0. K) by A6
.= f . (a1,b1) by RLVECT_1:def 4 ; :: thesis: verum

end;

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

end;

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

A12: now :: thesis: for ww being Vector of (VectQuot (W,(RKer f))) holds FunctionalSAF (ff,ww) is homogeneous

let ww be Vector of (VectQuot (W,(RKer f))); :: thesis: FunctionalSAF (ff,ww) is homogeneous
consider w being Vector of W such that
A13: ww = w + (RKer f) by VECTSP10:22;
set ffw = FunctionalSAF (ff,ww);

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

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

end;

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

end;

A16: CosetSet (W,(RKer f)) = the carrier of (VectQuot (W,(RKer f))) by VECTSP10:def 6;

A17: now :: thesis: for vv being Vector of (VectQuot (V,(LKer f))) holds FunctionalFAF (ff,vv) is homogeneous

let vv be Vector of (VectQuot (V,(LKer f))); :: thesis: FunctionalFAF (ff,vv) is homogeneous
consider v being Vector of V such that
A18: vv = v + (LKer f) by VECTSP10:22;
set ffv = FunctionalFAF (ff,vv);

now :: thesis: for A being Vector of (VectQuot (W,(RKer f)))
for r being Element of K holds (FunctionalFAF (ff,vv)) . (r * A) = r * ((FunctionalFAF (ff,vv)) . A)

let A be Vector of (VectQuot (W,(RKer f))); :: thesis: for r being Element of K holds (FunctionalFAF (ff,vv)) . (r * A) = r * ((FunctionalFAF (ff,vv)) . A)
let r be Element of K; :: thesis: (FunctionalFAF (ff,vv)) . (r * A) = r * ((FunctionalFAF (ff,vv)) . A)
consider a being Vector of W such that
A19: A = a + (RKer f) by VECTSP10:22;
A20: ( the lmult of (VectQuot (W,(RKer f))) = lmultCoset (W,(RKer f)) & (lmultCoset (W,(RKer f))) . (r,A) = (r * a) + (RKer f) ) by A16, A19, VECTSP10:def 5, VECTSP10:def 6;
thus (FunctionalFAF (ff,vv)) . (r * A) = ff . (vv,(r * A)) by Th8
.= f . (v,(r * a)) by A10, A18, A20
.= r * (f . (v,a)) by Th32
.= r * (ff . (vv,A)) by A10, A18, A19
.= r * ((FunctionalFAF (ff,vv)) . A) by Th8 ; :: thesis: verum

end;

hence FunctionalFAF (ff,vv) is homogeneous ; :: thesis: verum

end;

A21: now :: thesis: for ww being Vector of (VectQuot (W,(RKer f))) holds FunctionalSAF (ff,ww) is additive

let ww be Vector of (VectQuot (W,(RKer f))); :: thesis: FunctionalSAF (ff,ww) is additive
consider w being Vector of W such that
A22: ww = w + (RKer f) by VECTSP10:22;
set ffw = FunctionalSAF (ff,ww);

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

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

end;

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

end;

now :: thesis: for vv being Vector of (VectQuot (V,(LKer f))) holds FunctionalFAF (ff,vv) is additive

let vv be Vector of (VectQuot (V,(LKer f))); :: thesis: FunctionalFAF (ff,vv) is additive
consider v being Vector of V such that
A26: vv = v + (LKer f) by VECTSP10:22;
set ffv = FunctionalFAF (ff,vv);

now :: thesis: for A, B being Vector of (VectQuot (W,(RKer f))) holds (FunctionalFAF (ff,vv)) . (A + B) = ((FunctionalFAF (ff,vv)) . A) + ((FunctionalFAF (ff,vv)) . B)

let A, B be Vector of (VectQuot (W,(RKer f))); :: thesis: (FunctionalFAF (ff,vv)) . (A + B) = ((FunctionalFAF (ff,vv)) . A) + ((FunctionalFAF (ff,vv)) . B)
consider a being Vector of W such that
A27: A = a + (RKer f) by VECTSP10:22;
consider b being Vector of W such that
A28: B = b + (RKer f) by VECTSP10:22;
A29: ( the addF of (VectQuot (W,(RKer f))) = addCoset (W,(RKer f)) & (addCoset (W,(RKer f))) . (A,B) = (a + b) + (RKer f) ) by A16, A27, A28, VECTSP10:def 3, VECTSP10:def 6;
thus (FunctionalFAF (ff,vv)) . (A + B) = ff . (vv,(A + B)) by Th8
.= f . (v,(a + b)) by A10, A26, A29, RLVECT_1:2
.= (f . (v,a)) + (f . (v,b)) by Th27
.= (ff . (vv,A)) + (f . (v,b)) by A10, A26, A27
.= (ff . (vv,A)) + (ff . (vv,B)) by A10, A26, A28
.= ((FunctionalFAF (ff,vv)) . A) + (ff . (vv,B)) by Th8
.= ((FunctionalFAF (ff,vv)) . A) + ((FunctionalFAF (ff,vv)) . B) by Th8 ; :: thesis: verum

end;

hence FunctionalFAF (ff,vv) is additive ; :: thesis: verum

end;

then reconsider ff = ff as bilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer f))) by A21, A12, A17, Def11, Def12, Def13, Def14;
take ff ; :: thesis: for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
ff . (A,B) = f . (v,w)
thus for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
ff . (A,B) = f . (v,w) by A10; :: thesis: verum