let R be Ring; :: thesis: for V being LeftMod of R

for v being Vector of V

for u being object st u in Lin {v} holds

ex i being Element of R st u = i * v

let V be LeftMod of R; :: thesis: for v being Vector of V

for u being object st u in Lin {v} holds

ex i being Element of R st u = i * v

let v be Vector of V; :: thesis: for u being object st u in Lin {v} holds

ex i being Element of R st u = i * v

let u be object ; :: thesis: ( u in Lin {v} implies ex i being Element of R st u = i * v )

assume A1: u in Lin {v} ; :: thesis: ex i being Element of R st u = i * v

consider l being Linear_Combination of {v} such that

A2: u = Sum l by A1, VECTSP_7:7;

take l . v ; :: thesis: u = (l . v) * v

thus u = (l . v) * v by A2, VECTSP_6:17; :: thesis: verum

for v being Vector of V

for u being object st u in Lin {v} holds

ex i being Element of R st u = i * v

let V be LeftMod of R; :: thesis: for v being Vector of V

for u being object st u in Lin {v} holds

ex i being Element of R st u = i * v

let v be Vector of V; :: thesis: for u being object st u in Lin {v} holds

ex i being Element of R st u = i * v

let u be object ; :: thesis: ( u in Lin {v} implies ex i being Element of R st u = i * v )

assume A1: u in Lin {v} ; :: thesis: ex i being Element of R st u = i * v

consider l being Linear_Combination of {v} such that

A2: u = Sum l by A1, VECTSP_7:7;

take l . v ; :: thesis: u = (l . v) * v

thus u = (l . v) * v by A2, VECTSP_6:17; :: thesis: verum