let G be RealNormSpace-Sequence; :: thesis: for i being Element of dom G

for x, y being Point of (product G)

for xi, yi being Point of (G . i)

for zx, zy being Element of product (carr G) st xi = zx . i & zx = x & yi = zy . i & zy = y holds

||.(yi - xi).|| <= ||.(y - x).||

let i be Element of dom G; :: thesis: for x, y being Point of (product G)

for xi, yi being Point of (G . i)

for zx, zy being Element of product (carr G) st xi = zx . i & zx = x & yi = zy . i & zy = y holds

||.(yi - xi).|| <= ||.(y - x).||

let x, y be Point of (product G); :: thesis: for xi, yi being Point of (G . i)

for zx, zy being Element of product (carr G) st xi = zx . i & zx = x & yi = zy . i & zy = y holds

||.(yi - xi).|| <= ||.(y - x).||

let xi, yi be Point of (G . i); :: thesis: for zx, zy being Element of product (carr G) st xi = zx . i & zx = x & yi = zy . i & zy = y holds

||.(yi - xi).|| <= ||.(y - x).||

let zx, zy be Element of product (carr G); :: thesis: ( xi = zx . i & zx = x & yi = zy . i & zy = y implies ||.(yi - xi).|| <= ||.(y - x).|| )

assume that

A1: xi = zx . i and

A2: zx = x and

A3: yi = zy . i and

A4: zy = y ; :: thesis: ||.(yi - xi).|| <= ||.(y - x).||

reconsider zyi = zy . i, zxi = zx . i as Element of (G . i) by A1, A3;

A5: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6;

then reconsider mzx = - x as Element of product (carr G) ;

len G = len (carr G) by Def4;

then A6: dom G = dom (carr G) by FINSEQ_3:29;

- x = (- 1) * x by RLVECT_1:16;

then A7: mzx . i = (- jj) * zxi by A2, A5, A6, Lm4;

then reconsider mzxi = mzx . i as Element of (G . i) ;

reconsider zyMm = y - x as Element of product (carr G) by A5;

zyMm . i = zyi + mzxi by A4, A5, A6, Lm3;

then zyMm . i = zyi + (- zxi) by A7, RLVECT_1:16;

hence ||.(yi - xi).|| <= ||.(y - x).|| by A1, A3, Th10; :: thesis: verum

for x, y being Point of (product G)

for xi, yi being Point of (G . i)

for zx, zy being Element of product (carr G) st xi = zx . i & zx = x & yi = zy . i & zy = y holds

||.(yi - xi).|| <= ||.(y - x).||

let i be Element of dom G; :: thesis: for x, y being Point of (product G)

for xi, yi being Point of (G . i)

for zx, zy being Element of product (carr G) st xi = zx . i & zx = x & yi = zy . i & zy = y holds

||.(yi - xi).|| <= ||.(y - x).||

let x, y be Point of (product G); :: thesis: for xi, yi being Point of (G . i)

for zx, zy being Element of product (carr G) st xi = zx . i & zx = x & yi = zy . i & zy = y holds

||.(yi - xi).|| <= ||.(y - x).||

let xi, yi be Point of (G . i); :: thesis: for zx, zy being Element of product (carr G) st xi = zx . i & zx = x & yi = zy . i & zy = y holds

||.(yi - xi).|| <= ||.(y - x).||

let zx, zy be Element of product (carr G); :: thesis: ( xi = zx . i & zx = x & yi = zy . i & zy = y implies ||.(yi - xi).|| <= ||.(y - x).|| )

assume that

A1: xi = zx . i and

A2: zx = x and

A3: yi = zy . i and

A4: zy = y ; :: thesis: ||.(yi - xi).|| <= ||.(y - x).||

reconsider zyi = zy . i, zxi = zx . i as Element of (G . i) by A1, A3;

A5: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6;

then reconsider mzx = - x as Element of product (carr G) ;

len G = len (carr G) by Def4;

then A6: dom G = dom (carr G) by FINSEQ_3:29;

- x = (- 1) * x by RLVECT_1:16;

then A7: mzx . i = (- jj) * zxi by A2, A5, A6, Lm4;

then reconsider mzxi = mzx . i as Element of (G . i) ;

reconsider zyMm = y - x as Element of product (carr G) by A5;

zyMm . i = zyi + mzxi by A4, A5, A6, Lm3;

then zyMm . i = zyi + (- zxi) by A7, RLVECT_1:16;

hence ||.(yi - xi).|| <= ||.(y - x).|| by A1, A3, Th10; :: thesis: verum