set L = LKer f;
set vq = VectQuot (V,(LKer f));
set R = RKer f;
set wq = VectQuot (W,(RKer f));
let f1, f2 be bilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer f))); :: 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
f1 . (A,B) = f . (v,w) ) & ( 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
f2 . (A,B) = f . (v,w) ) implies f1 = f2 )
assume that
A30: 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
f1 . (A,B) = f . (v,w) and
A31: 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
f2 . (A,B) = f . (v,w) ; :: thesis: f1 = f2

now :: thesis: for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer f))) holds f1 . (A,B) = f2 . (A,B)

let A be Vector of (VectQuot (V,(LKer f))); :: thesis: for B being Vector of (VectQuot (W,(RKer f))) holds f1 . (A,B) = f2 . (A,B)
let B be Vector of (VectQuot (W,(RKer f))); :: thesis: f1 . (A,B) = f2 . (A,B)
consider a being Vector of V such that
A32: A = a + (LKer f) by VECTSP10:22;
consider b being Vector of W such that
A33: B = b + (RKer f) by VECTSP10:22;
thus f1 . (A,B) = f . (a,b) by A30, A32, A33
.= f2 . (A,B) by A31, A32, A33 ; :: thesis: verum

end;

hence f1 = f2 ; :: thesis: verum