let V be Z_Module; :: thesis: for v being Vector of V
for u being object st u in Lin {v} holds
ex i being Element of INT.Ring 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 INT.Ring st u = i * v
let u be object ; :: thesis: ( u in Lin {v} implies ex i being Element of INT.Ring st u = i * v )
assume u in Lin {v} ; :: thesis: ex i being Element of INT.Ring st u = i * v
then consider l being Linear_Combination of {v} such that
A1: u = Sum l by ZMODUL02:64;
take l . v ; :: thesis: u = (l . v) * v
thus u = (l . v) * v by A1, ZMODUL02:21; :: thesis: verum