let V be non empty RLSStruct ; :: thesis: for V1 being non empty add-closed multi-closed Subset of V
for a being Real
for v being VECTOR of V
for w being VECTOR of RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) st w = v holds
a * w = a * v
let V1 be non empty add-closed multi-closed Subset of V; :: thesis: for a being Real
for v being VECTOR of V
for w being VECTOR of RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) st w = v holds
a * w = a * v
let a be Real; :: thesis: for v being VECTOR of V
for w being VECTOR of RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) st w = v holds
a * w = a * v
let v be VECTOR of V; :: thesis: for w being VECTOR of RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) st w = v holds
a * w = a * v
let w be VECTOR of RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #); :: thesis: ( w = v implies a * w = a * v )
reconsider a = a as Element of REAL by XREAL_0:def 1;
assume A1: w = v ; :: thesis: a * w = a * v
then [a,v] in [:REAL,V1:] by ZFMISC_1:87;
hence a * w = a * v by A1, FUNCT_1:49; :: thesis: verum