let G be non-trivial RealNormSpace-Sequence; :: thesis: for i being Element of dom G
for x being Point of (product G)
for a being Element of REAL holds (proj i) . (a * x) = a * ((proj i) . x)
let i be Element of dom G; :: thesis: for x being Point of (product G)
for a being Element of REAL holds (proj i) . (a * x) = a * ((proj i) . x)
let x be Point of (product G); :: thesis: for a being Element of REAL holds (proj i) . (a * x) = a * ((proj i) . x)
let a be Element of REAL ; :: thesis: (proj i) . (a * x) = a * ((proj i) . x)
reconsider v = a * x as Element of product (carr G) by LM001;
reconsider s = x as Element of product (carr G) by LM001;
( (proj i) . (a * x) = v . i & (proj i) . x = s . i ) by Def1;
hence (proj i) . (a * x) = a * ((proj i) . x) by MLT1; :: thesis: verum