let V be strict Z_Module; :: 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