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 ) )

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

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 )

given v being VECTOR of V such that A1:
( x = v & L . v <> 0 )
; :: thesis: x in Carrier L( 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;( 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

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