let G be RealNormSpace-Sequence; :: thesis: for i being Element of dom G
for x being Point of (product G)
for a being 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 Real holds (proj i) . (a * x) = a * ((proj i) . x)
let x be Point of (product G); :: thesis: for a being Real holds (proj i) . (a * x) = a * ((proj i) . x)
let a be Real; :: thesis: (proj i) . (a * x) = a * ((proj i) . x)
reconsider a = a as Real ;
reconsider v = a * x as Element of product (carr G) by Th10;
reconsider s = x as Element of product (carr G) by Th10;
( (proj i) . (a * x) = v . i & (proj i) . x = s . i ) by Def3;
hence (proj i) . (a * x) = a * ((proj i) . x) by Th13; :: thesis: verum