let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for a being Real
for W being Subspace of V
for w being VECTOR of W st w = v holds
a * w = a * v
let v be VECTOR of V; :: thesis: for a being Real
for W being Subspace of V
for w being VECTOR of W st w = v holds
a * w = a * v
let a be Real; :: thesis: for W being Subspace of V
for w being VECTOR of W st w = v holds
a * w = a * v
let W be Subspace of V; :: thesis: for w being VECTOR of W st w = v holds
a * w = a * v
let w be VECTOR of W; :: thesis: ( w = v implies a * w = a * v )
assume A1: w = v ; :: thesis: a * w = a * v
reconsider aa = a as Element of REAL by XREAL_0:def 1;
aa * w = ( the Mult of V | [:REAL, the carrier of W:]) . [aa,w] by Def2;
then aa * w = aa * v by A1, FUNCT_1:49;
hence a * w = a * v ; :: thesis: verum