let p be Real; :: thesis: ( 1 <= p implies for lp being non empty NORMSTR st lp = NORMSTR(# ,,,,() #) holds
for x being Point of lp
for a being Real holds (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = |.a.| * ((Sum (() rto_power p)) to_power (1 / p)) )

assume A1: 1 <= p ; :: thesis: for lp being non empty NORMSTR st lp = NORMSTR(# ,,,,() #) holds
for x being Point of lp
for a being Real holds (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = |.a.| * ((Sum (() rto_power p)) to_power (1 / p))

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

assume A3: lp = NORMSTR(# ,,,,() #) ; :: thesis: for x being Point of lp
for a being Real holds (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = |.a.| * ((Sum (() rto_power p)) to_power (1 / p))

let x be Point of lp; :: thesis: for a being Real holds (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = |.a.| * ((Sum (() rto_power p)) to_power (1 / p))
A4: now :: thesis: for n being Nat holds (() rto_power p) . n >= 0
let n be Nat; :: thesis: (() rto_power p) . n >= 0
((seq_id x) rto_power p) . n = |.(() . n).| to_power p by Def1;
hence ((seq_id x) rto_power p) . n >= 0 by ; :: thesis: verum
end;
(seq_id x) rto_power p is summable by A1, A3, Th10;
then A5: 0 <= Sum (() rto_power p) by ;
let a be Real; :: thesis: (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = |.a.| * ((Sum (() rto_power p)) to_power (1 / p))
A6: |.a.| to_power p >= 0 by ;
thus (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = (() * (Sum (() rto_power p))) to_power (1 / p) by A1, A3, Lm6
.= (() to_power (1 / p)) * ((Sum (() rto_power p)) to_power (1 / p)) by A2, A5, A6, Lm2
.= (|.a.| to_power (p * (1 / p))) * ((Sum (() rto_power p)) to_power (1 / p)) by
.= () * ((Sum (() rto_power p)) to_power (1 / p)) by
.= |.a.| * ((Sum (() rto_power p)) to_power (1 / p)) by POWER:25 ; :: thesis: verum