let R be domRing; :: thesis: for V being LeftMod of R
for A being Subset of V
for W being strict Subspace of V st not R is degenerated & A = the carrier of W holds
Lin A = W
let V be LeftMod of R; :: thesis: for A being Subset of V
for W being strict Subspace of V st not R is degenerated & A = the carrier of W holds
Lin A = W
let A be Subset of V; :: thesis: for W being strict Subspace of V st not R is degenerated & A = the carrier of W holds
Lin A = W
let W be strict Subspace of V; :: thesis: ( not R is degenerated & A = the carrier of W implies Lin A = W )
assume that
not R is degenerated and
A2: A = the carrier of W ; :: thesis: Lin A = W
A1: 0. R <> 1. R ;

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 ) )
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 A2, 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 A2, Th8; :: thesis: verum

end;

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