let p be Real; :: thesis: ( 1 <= p implies for lp being non empty NORMSTR st lp = NORMSTR(# ,,,,() #) holds
for x, y being Point of lp
for a being Real holds
( ( = 0 implies x = 0. lp ) & ( x = 0. lp implies = 0 ) & 0 <= & ||.(x + y).|| <= + & ||.(a * x).|| = |.a.| * ) )

assume A1: 1 <= p ; :: thesis: for lp being non empty NORMSTR st lp = NORMSTR(# ,,,,() #) holds
for x, y being Point of lp
for a being Real holds
( ( = 0 implies x = 0. lp ) & ( x = 0. lp implies = 0 ) & 0 <= & ||.(x + y).|| <= + & ||.(a * x).|| = |.a.| * )

A2: 1 / p > 0 by ;
let lp be non empty NORMSTR ; :: thesis: ( lp = NORMSTR(# ,,,,() #) implies for x, y being Point of lp
for a being Real holds
( ( = 0 implies x = 0. lp ) & ( x = 0. lp implies = 0 ) & 0 <= & ||.(x + y).|| <= + & ||.(a * x).|| = |.a.| * ) )

assume A3: lp = NORMSTR(# ,,,,() #) ; :: thesis: for x, y being Point of lp
for a being Real holds
( ( = 0 implies x = 0. lp ) & ( x = 0. lp implies = 0 ) & 0 <= & ||.(x + y).|| <= + & ||.(a * x).|| = |.a.| * )

let x, y be Point of lp; :: thesis: for a being Real holds
( ( = 0 implies x = 0. lp ) & ( x = 0. lp implies = 0 ) & 0 <= & ||.(x + y).|| <= + & ||.(a * x).|| = |.a.| * )

A4: (seq_id y) rto_power p is summable by A1, A3, Th10;
A5: ||.y.|| = (Sum (() rto_power p)) to_power (1 / p) by ;
A6: ||.x.|| = (Sum (() rto_power p)) to_power (1 / p) by ;
A7: now :: thesis: ( = 0 implies x = 0. lp )
A8: ||.x.|| = (Sum (() rto_power p)) to_power (1 / p) by ;
A9: x in the_set_of_RealSequences by A1, A3, Def2;
assume A10: ||.x.|| = 0 ; :: thesis: x = 0. lp
(seq_id x) rto_power p is summable by A1, A3, Th10;
then for n being Nat holds 0 = () . n by A1, A10, A8, Th12;
hence x = Zeroseq by
.= 0. lp by A1, A3, Th10 ;
:: thesis: verum
end;
A11: (seq_id x) rto_power p is summable by A1, A3, Def2;
A12: (Sum (() rto_power p)) to_power (1 / p) = by ;
A13: now :: thesis: ( x = 0. lp implies = 0 )
assume x = 0. lp ; :: thesis:
then x = Zeroseq by A1, A3, Th10;
then A14: for n being Nat holds () . n = 0 by RSSPACE:4;
thus = (Sum (() rto_power p)) to_power (1 / p) by
.= 0 by ; :: thesis: verum
end;
let a be Real; :: thesis: ( ( = 0 implies x = 0. lp ) & ( x = 0. lp implies = 0 ) & 0 <= & ||.(x + y).|| <= + & ||.(a * x).|| = |.a.| * )
A15: for n being Nat holds 0 <= (() rto_power p) . n
proof
set xp = () rto_power p;
let n be Nat; :: thesis: 0 <= (() rto_power p) . n
A16: ( 0 < |.(() . n).| or 0 = |.(() . n).| ) by COMPLEX1:46;
((seq_id x) rto_power p) . n = |.(() . n).| to_power p by Def1;
hence 0 <= (() rto_power p) . n by ; :: thesis: verum
end;
() + () = seq_id (() + ())
.= seq_id (x + y) by A1, A3, Th10 ;
then A17: (Sum ((() + ()) rto_power p)) to_power (1 / p) = ||.(x + y).|| by ;
(seq_id x) rto_power p is summable by A1, A3, Th10;
then A18: ||.(x + y).|| <= + by A1, A6, A5, A17, A4, Th3;
A19: ||.x.|| = (Sum (() rto_power p)) to_power (1 / p) by ;
||.(a * x).|| = (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) by
.= |.a.| * by A1, A3, A19, Lm7 ;
hence ( ( ||.x.|| = 0 implies x = 0. lp ) & ( x = 0. lp implies = 0 ) & 0 <= & ||.(x + y).|| <= + & ||.(a * x).|| = |.a.| * ) by ; :: thesis: verum