let F be non degenerated almost_left_invertible Ring; :: thesis: for x being Scalar of F
for V being non empty right_complementable add-associative right_zeroed RightMod-like RightModStr over F
for v being Vector of V st x <> 0. F holds
(v * x) * (x ") = v
let x be Scalar of F; :: thesis: for V being non empty right_complementable add-associative right_zeroed RightMod-like RightModStr over F
for v being Vector of V st x <> 0. F holds
(v * x) * (x ") = v
let V be non empty right_complementable add-associative right_zeroed RightMod-like RightModStr over F; :: thesis: for v being Vector of V st x <> 0. F holds
(v * x) * (x ") = v
let v be Vector of V; :: thesis: ( x <> 0. F implies (v * x) * (x ") = v )
assume A1: x <> 0. F ; :: thesis: (v * x) * (x ") = v
(v * x) * (x ") = v * (x * (x ")) by Def8
.= v * (1_ F) by A1, Th9
.= v by Def8 ;
hence (v * x) * (x ") = v ; :: thesis: verum