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

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)

hence
f1 = f2
; :: thesis: verumfor 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;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