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 ( a <> 0 & u = (a " ) * v ) ; :: thesis: v = a * u
hence v = ((a " ) " ) * u by 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