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

A13: 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

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

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

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

A13: 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

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

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

now :: thesis: for A being Vector of (VectQuot (V,(LKer f)))

for w being Vector of W holds f1 . (A,w) = f2 . (A,w)

hence
f1 = f2
; :: thesis: verumfor w being Vector of W holds f1 . (A,w) = f2 . (A,w)

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

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

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

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

end;let w be Vector of W; :: thesis: f1 . (A,w) = f2 . (A,w)

consider a being Vector of V such that

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

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

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