let F be Field; :: thesis: for x being Element of F

for V being VectSp of F

for v being Element of V st x <> 0. F holds

(x ") * (x * v) = v

let x be Element of F; :: thesis: for V being VectSp of F

for v being Element of V st x <> 0. F holds

(x ") * (x * v) = v

let V be VectSp of F; :: thesis: for v being Element of V st x <> 0. F holds

(x ") * (x * v) = v

let v be Element of V; :: thesis: ( x <> 0. F implies (x ") * (x * v) = v )

assume A1: x <> 0. F ; :: thesis: (x ") * (x * v) = v

(x ") * (x * v) = ((x ") * x) * v by Def15

.= (1. F) * v by A1, Def10

.= v by Def16 ;

hence (x ") * (x * v) = v ; :: thesis: verum

for V being VectSp of F

for v being Element of V st x <> 0. F holds

(x ") * (x * v) = v

let x be Element of F; :: thesis: for V being VectSp of F

for v being Element of V st x <> 0. F holds

(x ") * (x * v) = v

let V be VectSp of F; :: thesis: for v being Element of V st x <> 0. F holds

(x ") * (x * v) = v

let v be Element of V; :: thesis: ( x <> 0. F implies (x ") * (x * v) = v )

assume A1: x <> 0. F ; :: thesis: (x ") * (x * v) = v

(x ") * (x * v) = ((x ") * x) * v by Def15

.= (1. F) * v by A1, Def10

.= v by Def16 ;

hence (x ") * (x * v) = v ; :: thesis: verum