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