let R be domRing; :: thesis: for V being RightMod of R
for A being Subset of V
for W being strict Submodule of V st 0. R <> 1_ R & A = the carrier of W holds
Lin A = W
let V be RightMod of R; :: thesis: for A being Subset of V
for W being strict Submodule of V st 0. R <> 1_ R & A = the carrier of W holds
Lin A = W
let A be Subset of V; :: thesis: for W being strict Submodule of V st 0. R <> 1_ R & A = the carrier of W holds
Lin A = W
let W be strict Submodule of V; :: thesis: ( 0. R <> 1_ R & A = the carrier of W implies Lin A = W )
assume that
A1: 0. R <> 1_ R and
A2: 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 ) )
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 Th67;
A is linearly-closed by A2, RMOD_2:33;
then v in the carrier of W by A1, A2, A3, Th29;
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, Th68; :: thesis: verum

end;

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