let n be non empty Nat; :: thesis: for x being Element of REAL n holds
( (sum_norm n) . x <= n * ((max_norm n) . x) & (max_norm n) . x <= |.x.| & |.x.| <= (sum_norm n) . x )
let x be Element of REAL n; :: thesis: ( (sum_norm n) . x <= n * ((max_norm n) . x) & (max_norm n) . x <= |.x.| & |.x.| <= (sum_norm n) . x )
set xMAX = (max_norm n) . x;
( (max_norm n) . x in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= (max_norm n) . x ) ) by Def1;
then ( Sum (abs x) <= n * ((max_norm n) . x) & (max_norm n) . x <= |.x.| & |.x.| <= Sum (abs x) ) by Th11;
hence ( (sum_norm n) . x <= n * ((max_norm n) . x) & (max_norm n) . x <= |.x.| & |.x.| <= (sum_norm n) . x ) by Def2; :: thesis: verum