let V be ComplexLinearSpace; :: thesis: for v being VECTOR of V
for z being Complex
for W being Subspace of V st v in W holds
z * v in v + W
let v be VECTOR of V; :: thesis: for z being Complex
for W being Subspace of V st v in W holds
z * v in v + W
let z be Complex; :: thesis: for W being Subspace of V st v in W holds
z * v in v + W
let W be Subspace of V; :: thesis: ( v in W implies z * v in v + W )
assume v in W ; :: thesis: z * v in v + W
then A1: (z - 1r) * v in W by Th41;
z * v = ((z - 1r) + 1r) * v
.= ((z - 1r) * v) + (1r * v) by Def3
.= v + ((z - 1r) * v) by Def5 ;
hence z * v in v + W by A1; :: thesis: verum