let G be RealNormSpace-Sequence; :: thesis: for x being Element of product (carr G)

for i being Element of NAT st i in dom x holds

0 <= (normsequence (G,x)) . i

let x be Element of product (carr G); :: thesis: for i being Element of NAT st i in dom x holds

0 <= (normsequence (G,x)) . i

let i be Element of 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 Def4

.= 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 Def4, 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

for i being Element of NAT st i in dom x holds

0 <= (normsequence (G,x)) . i

let x be Element of product (carr G); :: thesis: for i being Element of NAT st i in dom x holds

0 <= (normsequence (G,x)) . i

let i be Element of 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 Def4

.= 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 Def4, 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