begin
Lm1:
for R being Ring
for a being Scalar of R st - a = 0. R holds
a = 0. R
Lm2:
for R being Skew-Field
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 )
Lm3:
for R being Skew-Field
for V being LeftMod of R ex B being Subset of V st B is base