set L = LKer f;
set vq = VectQuot V,(LKer f);
set R = RKer (f *' );
set wq = VectQuot W,(RKer (f *' ));
let f1, f2 be sesquilinear-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
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
f1 . A,B = f . v,w and
A34: 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
A35: A = a + (LKer f) by VECTSP10:23;
consider b being Vector of W such that
A36: B = b + (RKer (f *' )) by VECTSP10:23;
thus f1 . A,B = f . a,b by A33, A35, A36
.= f2 . A,B by A34, A35, A36 ; :: thesis: verum

end;

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