let V be RealLinearSpace; :: thesis: for u, v being VECTOR of V
for a being Real holds
( ( a <> 0 & a * u = v implies u = (a " ) * v ) & ( a <> 0 & u = (a " ) * v implies a * u = v ) )
let u, v be VECTOR of V; :: thesis: for a being Real holds
( ( a <> 0 & a * u = v implies u = (a " ) * v ) & ( a <> 0 & u = (a " ) * v implies a * u = v ) )
let a be Real; :: thesis: ( ( a <> 0 & a * u = v implies u = (a " ) * v ) & ( a <> 0 & u = (a " ) * v implies a * u = v ) )

now

assume that
A1: a <> 0 and
A2: u = (a " ) * v ; :: thesis: v = a * u
thus v = ((a " ) " ) * u by A1, A2, Th12, XCMPLX_1:203
.= a * u ; :: thesis: verum

end;

hence ( ( a <> 0 & a * u = v implies u = (a " ) * v ) & ( a <> 0 & u = (a " ) * v implies a * u = v ) ) by Th12; :: thesis: verum