let G be RealNormSpace-Sequence; :: thesis: for i being Element of dom G
for x being Point of (product G) holds ||.((proj i) . x).|| <= ||.x.||
let i be Element of dom G; :: thesis: for x being Point of (product G) holds ||.((proj i) . x).|| <= ||.x.||
let x be Point of (product G); :: thesis: ||.((proj i) . x).|| <= ||.x.||
reconsider y = x as Element of product (carr G) by Th10;
(proj i) . x = y . i by Def3;
hence ||.((proj i) . x).|| <= ||.x.|| by PRVECT_2:10; :: thesis: verum