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