let V be RealLinearSpace; 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; 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; ( ( a <> 0 & a * u = v implies u = (a ") * v ) & ( a <> 0 & u = (a ") * v implies a * u = v ) )
hence
( ( a <> 0 & a * u = v implies u = (a ") * v ) & ( a <> 0 & u = (a ") * v implies a * u = v ) )
by Th5; verum