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

end;

hence f1 = f2 ; :: thesis: verum