let GF be Ring; :: thesis: for V being LeftMod of GF holds Lin ({} the carrier of V) = (0). V
let V be LeftMod of GF; :: thesis: Lin ({} the carrier of V) = (0). V
set A = Lin ({} the carrier of V);

now :: thesis: for v being Vector of V holds
( ( v in Lin ({} the carrier of V) implies v in (0). V ) & ( v in (0). V implies v in Lin ({} the carrier of V) ) )

let v be Vector of V; :: thesis: ( ( v in Lin ({} the carrier of V) implies v in (0). V ) & ( v in (0). V implies v in Lin ({} the carrier of V) ) )
thus ( v in Lin ({} the carrier of V) implies v in (0). V ) :: thesis: ( v in (0). V implies v in Lin ({} the carrier of V) )

proof

assume v in Lin ({} the carrier of V) ; :: thesis: v in (0). V
then A1: v in the carrier of (Lin ({} the carrier of V)) by STRUCT_0:def 5;
the carrier of (Lin ({} the carrier of V)) = { (Sum l0) where l0 is Linear_Combination of {} the carrier of V : verum } by Def2;
then ex l0 being Linear_Combination of {} the carrier of V st v = Sum l0 by A1;
then v = 0. V by VECTSP_6:16;
hence v in (0). V by VECTSP_4:35; :: thesis: verum

end;

assume v in (0). V ; :: thesis: v in Lin ({} the carrier of V)
then v = 0. V by VECTSP_4:35;
hence v in Lin ({} the carrier of V) by VECTSP_4:17; :: thesis: verum

end;

hence Lin ({} the carrier of V) = (0). V by VECTSP_4:30; :: thesis: verum