let p be Real; :: thesis: ( 1 <= p implies for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ (the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences ),(l_norm^ p) #) holds
for x being Point of lp
for a being Real holds (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = (abs a) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p)) )
assume A1: 1 <= p ; :: thesis: for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ (the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences ),(l_norm^ p) #) holds
for x being Point of lp
for a being Real holds (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = (abs a) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p))
let lp be non empty NORMSTR ; :: thesis: ( lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ (the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences ),(l_norm^ p) #) implies for x being Point of lp
for a being Real holds (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = (abs a) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p)) )
assume A2: lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ (the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences ),(l_norm^ p) #) ; :: thesis: for x being Point of lp
for a being Real holds (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = (abs a) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p))
A3: 1 / p > 0 by A1, XREAL_1:141;
let x be Point of lp; :: thesis: for a being Real holds (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = (abs a) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p))
let a be Real; :: thesis: (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = (abs a) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p))
A4: (seq_id x) rto_power p is summable by A1, A2, Th10;

now

let n be Element of NAT ; :: thesis: ((seq_id x) rto_power p) . n >= 0
((seq_id x) rto_power p) . n = (abs ((seq_id x) . n)) to_power p by Def1;
hence ((seq_id x) rto_power p) . n >= 0 by A1, Lm1, COMPLEX1:132; :: thesis: verum

end;

then A5: 0 <= Sum ((seq_id x) rto_power p) by A4, SERIES_1:21;
A6: (abs a) to_power p >= 0 by A1, Lm1, COMPLEX1:132;
thus (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = (((abs a) to_power p) * (Sum ((seq_id x) rto_power p))) to_power (1 / p) by A1, A2, Lm7
.= (((abs a) to_power p) to_power (1 / p)) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p)) by A3, A5, A6, Lm2
.= ((abs a) to_power (p * (1 / p))) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p)) by A1, A3, COMPLEX1:132, HOLDER_1:2
.= ((abs a) to_power 1) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p)) by A1, XCMPLX_1:107
.= (abs a) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p)) by POWER:30 ; :: thesis: verum