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