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

for i being Nat st i in dom x & z = [:(addop G):] . (x,y) holds

(normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i

let x, y, z be Element of product (carr G); :: thesis: for i being Nat st i in dom x & z = [:(addop G):] . (x,y) holds

(normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i

let i be Nat; :: thesis: ( i in dom x & z = [:(addop G):] . (x,y) implies (normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i )

assume that

A1: i in dom x and

A2: z = [:(addop G):] . (x,y) ; :: thesis: (normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i

reconsider i0 = i as Element of dom (carr G) by A1, CARD_3:9;

A3: z . i0 = ((addop G) . i0) . ((x . i0),(y . i0)) by A2, PRVECT_1:def 8;

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, yi0 = y . i0, zi0 = z . i0 as Element of (G . i0) by A1, CARD_3:9;

||.zi0.|| = ||.(xi0 + yi0).|| by A3, PRVECT_1:def 12;

then A4: ||.zi0.|| <= ||.xi0.|| + ||.yi0.|| by NORMSP_1:def 1;

A5: ((normsequence (G,x)) . i0) + ((normsequence (G,y)) . i0) = ((normsequence (G,x)) + (normsequence (G,y))) . i0 by RVSUM_1:11;

( the normF of (G . i0) . yi0 = (normsequence (G,y)) . i0 & the normF of (G . i0) . zi0 = (normsequence (G,z)) . i0 ) by Def11;

hence (normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i by A4, A5, Def11; :: thesis: verum

for i being Nat st i in dom x & z = [:(addop G):] . (x,y) holds

(normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i

let x, y, z be Element of product (carr G); :: thesis: for i being Nat st i in dom x & z = [:(addop G):] . (x,y) holds

(normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i

let i be Nat; :: thesis: ( i in dom x & z = [:(addop G):] . (x,y) implies (normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i )

assume that

A1: i in dom x and

A2: z = [:(addop G):] . (x,y) ; :: thesis: (normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i

reconsider i0 = i as Element of dom (carr G) by A1, CARD_3:9;

A3: z . i0 = ((addop G) . i0) . ((x . i0),(y . i0)) by A2, PRVECT_1:def 8;

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, yi0 = y . i0, zi0 = z . i0 as Element of (G . i0) by A1, CARD_3:9;

||.zi0.|| = ||.(xi0 + yi0).|| by A3, PRVECT_1:def 12;

then A4: ||.zi0.|| <= ||.xi0.|| + ||.yi0.|| by NORMSP_1:def 1;

A5: ((normsequence (G,x)) . i0) + ((normsequence (G,y)) . i0) = ((normsequence (G,x)) + (normsequence (G,y))) . i0 by RVSUM_1:11;

( the normF of (G . i0) . yi0 = (normsequence (G,y)) . i0 & the normF of (G . i0) . zi0 = (normsequence (G,z)) . i0 ) by Def11;

hence (normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i by A4, A5, Def11; :: thesis: verum