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
A32: 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
A33: 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

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
A34: A = a + (LKer f) by VECTSP10:23;
consider b being Vector of W such that
A35: B = b + (RKer f) by VECTSP10:23;
thus f1 . A,B = f . a,b by A32, A34, A35
.= f2 . A,B by A33, A34, A35 ; :: thesis: verum

end;

hence f1 = f2 by BINOP_1:2; :: thesis: verum