let V be ComplexLinearSpace; :: thesis: for v being VECTOR of V
for z1, z2 being Complex st v <> 0. V & z1 * v = z2 * v holds
z1 = z2
let v be VECTOR of V; :: thesis: for z1, z2 being Complex st v <> 0. V & z1 * v = z2 * v holds
z1 = z2
let z1, z2 be Complex; :: thesis: ( v <> 0. V & z1 * v = z2 * v implies z1 = z2 )
assume that
A1: v <> 0. V and
A2: z1 * v = z2 * v ; :: thesis: z1 = z2
0. V = (z1 * v) - (z2 * v) by A2, RLVECT_1:15
.= (z1 - z2) * v by Th10 ;
then (- z2) + z1 = 0 by A1, Th2;
hence z1 = z2 ; :: thesis: verum