let R be Ring; :: thesis: for V being strict LeftMod of R

for A being Subset of V st A = the carrier of V holds

Lin A = V

let V be strict LeftMod of R; :: thesis: for A being Subset of V st A = the carrier of V holds

Lin A = V

let A be Subset of V; :: thesis: ( A = the carrier of V implies Lin A = V )

assume A = the carrier of V ; :: thesis: Lin A = V

then for v being Vector of V holds

( v in Lin A iff v in (Omega). V ) by Th65;

hence Lin A = V by ZMODUL01:46; :: thesis: verum

for A being Subset of V st A = the carrier of V holds

Lin A = V

let V be strict LeftMod of R; :: thesis: for A being Subset of V st A = the carrier of V holds

Lin A = V

let A be Subset of V; :: thesis: ( A = the carrier of V implies Lin A = V )

assume A = the carrier of V ; :: thesis: Lin A = V

then for v being Vector of V holds

( v in Lin A iff v in (Omega). V ) by Th65;

hence Lin A = V by ZMODUL01:46; :: thesis: verum