let V be non trivial free Z_Module; :: thesis: for v being non zero Vector of V
for I being Basis of V ex L being Linear_Combination of I ex u being Vector of V st
( v = Sum L & u in I & L . u <> 0 )
let v be non zero Vector of V; :: thesis: for I being Basis of V ex L being Linear_Combination of I ex u being Vector of V st
( v = Sum L & u in I & L . u <> 0 )
let I be Basis of V; :: thesis: ex L being Linear_Combination of I ex u being Vector of V st
( v = Sum L & u in I & L . u <> 0 )
A1: ( I is linearly-independent & (Omega). V = Lin I ) by VECTSP_7:def 3;
v in Lin I by A1;
then consider L being Linear_Combination of I such that
A2: v = Sum L by ZMODUL02:64;
Carrier L <> {}
proof
assume Carrier L = {} ; :: thesis: contradiction
then Sum L = 0. V by ZMODUL02:23;
hence contradiction by A2; :: 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= I by VECTSP_6:def 4;
take L ; :: thesis: ex u being Vector of V st
( v = Sum L & u in I & L . u <> 0 )
take u ; :: thesis: ( v = Sum L & u in I & L . u <> 0 )
thus ( v = Sum L & u in I & L . u <> 0 ) by A2, A3, A4, A5; :: thesis: verum