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) = () * (Sum (() rto_power 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) = () * (Sum (() rto_power p))

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) = () * (Sum (() rto_power p)) )

assume A2: lp = NORMSTR(# ,,,,() #) ; :: thesis: for x being Point of lp
for a being Real holds Sum ((seq_id (a * x)) rto_power p) = () * (Sum (() rto_power p))

let x be Point of lp; :: thesis: for a being Real holds Sum ((seq_id (a * x)) rto_power p) = () * (Sum (() rto_power p))
A3: (seq_id x) rto_power p is summable by A1, A2, Th10;
let a be Real; :: thesis: Sum ((seq_id (a * x)) rto_power p) = () * (Sum (() rto_power p))
thus Sum ((seq_id (a * x)) rto_power p) = Sum (() (#) (() rto_power p)) by A1, A2, Lm5
.= () * (Sum (() rto_power p)) by ; :: thesis: verum