let V be RealLinearSpace; :: 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 RLVECT_2:31;
hence v in (0). V by Lm2; :: thesis: verum

end;

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

end;

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