let V be RealUnitarySpace; :: 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 Def1;
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 Lm1; :: thesis: verum

end;

assume v in (0). V ; :: thesis: v in Lin ({} the carrier of V)
then v = 0. V by Lm1;
hence v in Lin ({} the carrier of V) by RUSUB_1:11; :: thesis: verum

end;

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