set L = RKer f;

set vq = VectQuot (W,(RKer f));

let f1, f2 be additiveFAF homogeneousFAF Form of V,(VectQuot (W,(RKer f))); :: thesis: ( ( for A being Vector of (VectQuot (W,(RKer f)))

for v being Vector of V

for w being Vector of W st A = w + (RKer f) holds

f1 . (v,A) = f . (v,w) ) & ( for A being Vector of (VectQuot (W,(RKer f)))

for v being Vector of V

for w being Vector of W st A = w + (RKer f) holds

f2 . (v,A) = f . (v,w) ) implies f1 = f2 )

assume that

A13: for A being Vector of (VectQuot (W,(RKer f)))

for v being Vector of V

for a being Vector of W st A = a + (RKer f) holds

f1 . (v,A) = f . (v,a) and

A14: for A being Vector of (VectQuot (W,(RKer f)))

for v being Vector of V

for a being Vector of W st A = a + (RKer f) holds

f2 . (v,A) = f . (v,a) ; :: thesis: f1 = f2

set vq = VectQuot (W,(RKer f));

let f1, f2 be additiveFAF homogeneousFAF Form of V,(VectQuot (W,(RKer f))); :: thesis: ( ( for A being Vector of (VectQuot (W,(RKer f)))

for v being Vector of V

for w being Vector of W st A = w + (RKer f) holds

f1 . (v,A) = f . (v,w) ) & ( for A being Vector of (VectQuot (W,(RKer f)))

for v being Vector of V

for w being Vector of W st A = w + (RKer f) holds

f2 . (v,A) = f . (v,w) ) implies f1 = f2 )

assume that

A13: for A being Vector of (VectQuot (W,(RKer f)))

for v being Vector of V

for a being Vector of W st A = a + (RKer f) holds

f1 . (v,A) = f . (v,a) and

A14: for A being Vector of (VectQuot (W,(RKer f)))

for v being Vector of V

for a being Vector of W st A = a + (RKer f) holds

f2 . (v,A) = f . (v,a) ; :: thesis: f1 = f2

now :: thesis: for v being Vector of V

for A being Vector of (VectQuot (W,(RKer f))) holds f1 . (v,A) = f2 . (v,A)

hence
f1 = f2
; :: thesis: verumfor A being Vector of (VectQuot (W,(RKer f))) holds f1 . (v,A) = f2 . (v,A)

let v be Vector of V; :: thesis: for A being Vector of (VectQuot (W,(RKer f))) holds f1 . (v,A) = f2 . (v,A)

let A be Vector of (VectQuot (W,(RKer f))); :: thesis: f1 . (v,A) = f2 . (v,A)

consider a being Vector of W such that

A15: A = a + (RKer f) by VECTSP10:22;

thus f1 . (v,A) = f . (v,a) by A13, A15

.= f2 . (v,A) by A14, A15 ; :: thesis: verum

end;let A be Vector of (VectQuot (W,(RKer f))); :: thesis: f1 . (v,A) = f2 . (v,A)

consider a being Vector of W such that

A15: A = a + (RKer f) by VECTSP10:22;

thus f1 . (v,A) = f . (v,a) by A13, A15

.= f2 . (v,A) by A14, A15 ; :: thesis: verum