set L = LKer f;
set vq = VectQuot V,(LKer f);
let f1, f2 be additiveSAF homogeneousSAF Form of (VectQuot V,(LKer f)),W; :: thesis: ( ( for A being Vector of (VectQuot V,(LKer f))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
f1 . A,w = f . v,w ) & ( for A being Vector of (VectQuot V,(LKer f))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
f2 . A,w = f . v,w ) implies f1 = f2 )
assume that
A14: for A being Vector of (VectQuot V,(LKer f))
for w being Vector of W
for a being Vector of V st A = a + (LKer f) holds
f1 . A,w = f . a,w and
A15: for A being Vector of (VectQuot V,(LKer f))
for w being Vector of W
for a being Vector of V st A = a + (LKer f) holds
f2 . A,w = f . a,w ; :: thesis: f1 = f2

now

let A be Vector of (VectQuot V,(LKer f)); :: thesis: for w being Vector of W holds f1 . A,w = f2 . A,w
let w be Vector of W; :: thesis: f1 . A,w = f2 . A,w
consider a being Vector of V such that
A16: A = a + (LKer f) by VECTSP10:23;
thus f1 . A,w = f . a,w by A14, A16
.= f2 . A,w by A15, A16 ; :: thesis: verum

end;

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