let R be Ring; :: thesis: for V being RightMod of R
for V1 being Subset of V st V1 is linearly-closed holds
for v being Vector of V st v in V1 holds
- v in V1
let V be RightMod of R; :: thesis: for V1 being Subset of V st V1 is linearly-closed holds
for v being Vector of V st v in V1 holds
- v in V1
let V1 be Subset of V; :: thesis: ( V1 is linearly-closed implies for v being Vector of V st v in V1 holds
- v in V1 )
assume A1: V1 is linearly-closed ; :: thesis: for v being Vector of V st v in V1 holds
- v in V1
let v be Vector of V; :: thesis: ( v in V1 implies - v in V1 )
assume v in V1 ; :: thesis: - v in V1
then v * (- (1_ R)) in V1 by A1;
hence - v in V1 by VECTSP_2:32; :: thesis: verum