let GF be non degenerated Ring; :: thesis: for V being LeftMod of GF
for A being Subset of V
for W being strict Subspace of V st A = the carrier of W holds
Lin A = W
let V be LeftMod of GF; :: thesis: for A being Subset of V
for W being strict Subspace of V st A = the carrier of W holds
Lin A = W
let A be Subset of V; :: thesis: for W being strict Subspace of V st A = the carrier of W holds
Lin A = W
let W be strict Subspace of V; :: thesis: ( A = the carrier of W implies Lin A = W )
assume A1: A = the carrier of W ; :: thesis: Lin A = W

now :: thesis: for v being Vector of V holds
( ( v in Lin A implies v in W ) & ( v in W implies v in Lin A ) )

let v be Vector of V; :: thesis: ( ( v in Lin A implies v in W ) & ( v in W implies v in Lin A ) )
A2: 0. GF <> 1. GF ;
thus ( v in Lin A implies v in W ) :: thesis: ( v in W implies v in Lin A )

proof

assume v in Lin A ; :: thesis: v in W
then A3: ex l being Linear_Combination of A st v = Sum l by Th7;
A is linearly-closed by A1, VECTSP_4:33;
then v in the carrier of W by A1, A2, A3, VECTSP_6:14;
hence v in W by STRUCT_0:def 5; :: thesis: verum

end;

( v in W iff v in the carrier of W ) by STRUCT_0:def 5;
hence ( v in W implies v in Lin A ) by A1, Th8; :: thesis: verum

end;

hence Lin A = W by VECTSP_4:30; :: thesis: verum