let G be RealNormSpace-Sequence; :: thesis: for x, y, z being Element of product (carr G)
for i being Element of 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 Element of 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 Element of 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:18;
A3: z . i0 = ((addop G) . i0) . (x . i0),(y . i0) by A2, PRVECT_1:def 10;
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:18;
( dom x = dom (carr G) & (carr G) . i0 = the carrier of (G . i0) ) by Def4, CARD_3:18;
then reconsider xi0 = x . i0, yi0 = y . i0, zi0 = z . i0 as Element of (G . i0) by A1, CARD_3:18;
||.zi0.|| = ||.(xi0 + yi0).|| by A3, Def5;
then A4: ||.zi0.|| <= ||.xi0.|| + ||.yi0.|| by NORMSP_1:def 2;
A5: ((normsequence G,x) . i0) + ((normsequence G,y) . i0) = ((normsequence G,x) + (normsequence G,y)) . i0 by RVSUM_1:27;
( 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