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 ) )

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 )

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

hence v = ((a ") ") * u by Th5, XCMPLX_1:202

.= a * u ;

:: thesis: verum

end;hence v = ((a ") ") * u by Th5, XCMPLX_1:202

.= a * u ;

:: thesis: verum