let K be Field; :: thesis: for V being VectSp of K

for v being Vector of V

for a, b being Scalar of st v <> 0. V & a * v = b * v holds

a = b

let V be VectSp of K; :: thesis: for v being Vector of V

for a, b being Scalar of st v <> 0. V & a * v = b * v holds

a = b

let v be Vector of V; :: thesis: for a, b being Scalar of st v <> 0. V & a * v = b * v holds

a = b

let a, b be Scalar of ; :: thesis: ( v <> 0. V & a * v = b * v implies a = b )

assume that

A1: v <> 0. V and

A2: a * v = b * v ; :: thesis: a = b

(a * v) - (b * v) = 0. V by A2, VECTSP_1:19;

then (a - b) * v = 0. V by VECTSP_4:82;

then a - b = 0. K by A1, VECTSP_1:15;

hence a = b by VECTSP_1:19; :: thesis: verum

for v being Vector of V

for a, b being Scalar of st v <> 0. V & a * v = b * v holds

a = b

let V be VectSp of K; :: thesis: for v being Vector of V

for a, b being Scalar of st v <> 0. V & a * v = b * v holds

a = b

let v be Vector of V; :: thesis: for a, b being Scalar of st v <> 0. V & a * v = b * v holds

a = b

let a, b be Scalar of ; :: thesis: ( v <> 0. V & a * v = b * v implies a = b )

assume that

A1: v <> 0. V and

A2: a * v = b * v ; :: thesis: a = b

(a * v) - (b * v) = 0. V by A2, VECTSP_1:19;

then (a - b) * v = 0. V by VECTSP_4:82;

then a - b = 0. K by A1, VECTSP_1:15;

hence a = b by VECTSP_1:19; :: thesis: verum