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
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
f1 . v,A = f . v,a and
A15: 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

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
A16: A = a + (RKer f) by VECTSP10:23;
thus f1 . v,A = f . v,a by A14, A16
.= f2 . v,A by A15, A16 ; :: thesis: verum

end;

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