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