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 Def2
.= v + ((z - 1r ) * v) by Def2 ;
hence z * v in v + W by A1; :: thesis: verum