let F be non degenerated almost_left_invertible Ring; :: thesis: for x being Scalar of F
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ModuleStr over 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 vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ModuleStr over F
for v being Vector of V st x <> 0. F holds
(x ") * (x * v) = v
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ModuleStr over 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 16
.= (1_ F) * v by A1, Th9
.= v by VECTSP_1:def 17 ;
hence (x ") * (x * v) = v ; :: thesis: verum