let V be non trivial torsion-free Z_Module; :: thesis: for v being non zero Vector of V
for A being Subset of V
for a being Element of INT.Ring st a in NAT & A is linearly-independent & a > 0 & a * v in Lin A holds
ex L being Linear_Combination of A ex u being Vector of V st
( a * v = Sum L & u in A & L . u <> 0 )
let v be non zero Vector of V; :: thesis: for A being Subset of V
for a being Element of INT.Ring st a in NAT & A is linearly-independent & a > 0 & a * v in Lin A holds
ex L being Linear_Combination of A ex u being Vector of V st
( a * v = Sum L & u in A & L . u <> 0 )
let A be Subset of V; :: thesis: for a being Element of INT.Ring st a in NAT & A is linearly-independent & a > 0 & a * v in Lin A holds
ex L being Linear_Combination of A ex u being Vector of V st
( a * v = Sum L & u in A & L . u <> 0 )
let a be Element of INT.Ring; :: thesis: ( a in NAT & A is linearly-independent & a > 0 & a * v in Lin A implies ex L being Linear_Combination of A ex u being Vector of V st
( a * v = Sum L & u in A & L . u <> 0 ) )
assume A1: ( a in NAT & A is linearly-independent & a > 0 & a * v in Lin A ) ; :: thesis: ex L being Linear_Combination of A ex u being Vector of V st
( a * v = Sum L & u in A & L . u <> 0 )
a1: a <> 0. INT.Ring by A1;
consider L being Linear_Combination of A such that
A2: a * v = Sum L by A1, ZMODUL02:64;
Carrier L <> {}

proof

assume Carrier L = {} ; :: thesis: contradiction
then Sum L = 0. V by ZMODUL02:23;
hence contradiction by a1, A2, ZMODUL01:def 7; :: thesis: verum

end;

then consider uu being object such that
A3: uu in Carrier L by XBOOLE_0:def 1;
consider u being Vector of V such that
A4: ( u = uu & L . u <> 0 ) by A3;
A5: Carrier L c= A by VECTSP_6:def 4;
take L ; :: thesis: ex u being Vector of V st
( a * v = Sum L & u in A & L . u <> 0 )
take u ; :: thesis: ( a * v = Sum L & u in A & L . u <> 0 )
thus ( a * v = Sum L & u in A & L . u <> 0 ) by A2, A3, A4, A5; :: thesis: verum