let R be Skew-Field; :: thesis: for a being Scalar of R
for V being LeftMod of R
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 R; :: thesis: for V being LeftMod of R
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 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 ;
:: thesis: ((a ") * a) * v = (1. R) * v
thus ((a ") * a) * v = (1. R) * v by A1, VECTSP_2:9; :: thesis: verum