let R be non degenerated almost_left_invertible Ring; :: thesis: for V being LeftMod of R
for a being Scalar of
for v being Vector of V st a <> 0. R holds
( (a ") * (a * v) = (1. R) * v & ((a ") * a) * v = (1. R) * v )
let V be LeftMod of R; :: thesis: for a being Scalar of
for v being Vector of V st a <> 0. R holds
( (a ") * (a * v) = (1. R) * v & ((a ") * a) * v = (1. R) * v )
let a be Scalar of ; :: thesis: for v being Vector of V st a <> 0. R holds
( (a ") * (a * v) = (1. R) * v & ((a ") * a) * v = (1. R) * v )
let v be Vector of V; :: thesis: ( a <> 0. R implies ( (a ") * (a * v) = (1. R) * v & ((a ") * a) * v = (1. R) * v ) )
assume A1: a <> 0. R ; :: thesis: ( (a ") * (a * v) = (1. R) * v & ((a ") * a) * v = (1. R) * v )
hence (a ") * (a * v) = v by VECTSP_2:31
.= (1. R) * v by VECTSP_1:def 17 ;
:: thesis: ((a ") * a) * v = (1. R) * v
thus ((a ") * a) * v = (1. R) * v by A1, VECTSP_2:9; :: thesis: verum