let V be ComplexLinearSpace; :: thesis: for v being VECTOR of V
for z being Complex
for W being Subspace of V
for w being VECTOR of W st w = v holds
z * w = z * v
let v be VECTOR of V; :: thesis: for z being Complex
for W being Subspace of V
for w being VECTOR of W st w = v holds
z * w = z * v
let z be Complex; :: thesis: for W being Subspace of V
for w being VECTOR of W st w = v holds
z * w = z * v
let W be Subspace of V; :: thesis: for w being VECTOR of W st w = v holds
z * w = z * v
let w be VECTOR of W; :: thesis: ( w = v implies z * w = z * v )
reconsider z = z as Element of COMPLEX by XCMPLX_0:def 2;
z * w = ( the Mult of V | [:COMPLEX, the carrier of W:]) . [z,w] by Def8;
hence ( w = v implies z * w = z * v ) by FUNCT_1:49; :: thesis: verum