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 *')))); ( ( 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)
; f1 = f2
now 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)));
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 *'))));
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
;
verum end;
hence
f1 = f2
; verum