let V be RealLinearSpace; :: thesis: for u, v being VECTOR of V
for a being Real st a <> 0 & a * u = v holds
u = (a ") * v
let u, v be VECTOR of V; :: thesis: for a being Real st a <> 0 & a * u = v holds
u = (a ") * v
let a be Real; :: thesis: ( a <> 0 & a * u = v implies u = (a ") * v )
assume that
A1: a <> 0 and
A2: a * u = v ; :: thesis: u = (a ") * v
thus u = 1 * u by RLVECT_1:def 8
.= ((a ") * a) * u by A1, XCMPLX_0:def 7
.= (a ") * v by A2, RLVECT_1:def 7 ; :: thesis: verum