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
for B being Vector of
for v being Vector of
for w being Vector of st A = v + (LKer f) & B = w + (RKer (f *' )) holds
f1 . A,B = f . v,w ) & ( for A being Vector of
for B being Vector of
for v being Vector of
for w being Vector of st A = v + (LKer f) & B = w + (RKer (f *' )) holds
f2 . A,B = f . v,w ) implies f1 = f2 )
assume that
A31: for A being Vector of
for B being Vector of
for v being Vector of
for w being Vector of st A = v + (LKer f) & B = w + (RKer (f *' )) holds
f1 . A,B = f . v,w and
A32: for A being Vector of
for B being Vector of
for v being Vector of
for w being Vector of 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 ; :: thesis: for B being Vector of holds f1 . A,B = f2 . A,B
let B be Vector of ; :: thesis: f1 . A,B = f2 . A,B
consider a being Vector of such that
A33: A = a + (LKer f) by VECTSP10:23;
consider b being Vector of such that
A34: B = b + (RKer (f *' )) by VECTSP10:23;
thus f1 . A,B = f . a,b by A31, A33, A34
.= f2 . A,B by A32, A33, A34 ; :: thesis: verum

end;

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