let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V
for x being VECTOR of V holds
( x in Carrier L iff ex v being VECTOR of V st
( x = v & L . v <> 0 ) )
let L be Linear_Combination of V; :: thesis: for x being VECTOR of V holds
( x in Carrier L iff ex v being VECTOR of V st
( x = v & L . v <> 0 ) )
let x be VECTOR of V; :: thesis: ( x in Carrier L iff ex v being VECTOR of V st
( x = v & L . v <> 0 ) )

hereby :: thesis: ( ex v being VECTOR of V st
( x = v & L . v <> 0 ) implies x in Carrier L )

assume x in Carrier L ; :: thesis: ex v being VECTOR of V st
( x = v & L . v <> 0 )
then x in { w where w is VECTOR of V : L . w <> 0 } by RLVECT_2:def 4;
hence ex v being VECTOR of V st
( x = v & L . v <> 0 ) ; :: thesis: verum

end;

given v being VECTOR of V such that A1: ( x = v & L . v <> 0 ) ; :: thesis: x in Carrier L
x in { w where w is VECTOR of V : L . w <> 0 } by A1;
hence x in Carrier L by RLVECT_2:def 4; :: thesis: verum