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 PRVECT_1:def 11;
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