let G be RealNormSpace-Sequence; :: thesis: for x being Element of product (carr G)
for i being Nat st i in dom x holds
0 <= (normsequence (G,x)) . i
let x be Element of product (carr G); :: thesis: for i being Nat st i in dom x holds
0 <= (normsequence (G,x)) . i
let i be Nat; :: thesis: ( i in dom x implies 0 <= (normsequence (G,x)) . i )
assume A1: i in dom x ; :: thesis: 0 <= (normsequence (G,x)) . i
dom G = Seg (len G) by FINSEQ_1:def 3
.= Seg (len (carr G)) by PRVECT_1:def 11
.= dom (carr G) by FINSEQ_1:def 3 ;
then reconsider i0 = i as Element of dom G by A1, CARD_3:9;
( dom x = dom (carr G) & (carr G) . i0 = the carrier of (G . i0) ) by PRVECT_1:def 11, CARD_3:9;
then reconsider xi0 = x . i0 as Element of (G . i0) by A1, CARD_3:9;
0 <= ||.xi0.|| by NORMSP_1:4;
hence 0 <= (normsequence (G,x)) . i by Def11; :: thesis: verum