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

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