let F be non degenerated almost_left_invertible Ring; :: thesis: for x being Scalar of F
for V being non empty right_complementable VectSp-like add-associative right_zeroed VectSpStr of F
for v being Vector of V st x <> 0. F holds
(x " ) * (x * v) = v
let x be Scalar of F; :: thesis: for V being non empty right_complementable VectSp-like add-associative right_zeroed VectSpStr of F
for v being Vector of V st x <> 0. F holds
(x " ) * (x * v) = v
let V be non empty right_complementable VectSp-like add-associative right_zeroed VectSpStr of F; :: thesis: for v being Vector of V st x <> 0. F holds
(x " ) * (x * v) = v
let v be Vector 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 VECTSP_1:def 26
.= (1_ F) * v by A1, Th43
.= v by VECTSP_1:def 26 ;
hence (x " ) * (x * v) = v ; :: thesis: verum