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

assume ( a <> 0 & u = (a ") * v ) ; :: thesis: v = a * u
hence v = ((a ") ") * u by Th5, XCMPLX_1:202
.= 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 Th5; :: thesis: verum