let p be Real; ( 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) = |.a.| * ((Sum ((seq_id x) rto_power p)) to_power (1 / p)) )
assume A1:
1 <= p
; 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) = |.a.| * ((Sum ((seq_id x) rto_power p)) to_power (1 / p))
A2:
1 / p > 0
by A1, XREAL_1:139;
let lp be non empty NORMSTR ; ( 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) = |.a.| * ((Sum ((seq_id x) rto_power p)) to_power (1 / p)) )
assume A3:
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) #)
; 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 ((seq_id x) rto_power p)) to_power (1 / p))
let x be Point of lp; for a being Real holds (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = |.a.| * ((Sum ((seq_id x) rto_power p)) to_power (1 / p))
(seq_id x) rto_power p is summable
by A1, A3, Th10;
then A5:
0 <= Sum ((seq_id x) rto_power p)
by A4, SERIES_1:18;
let a be Real; (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = |.a.| * ((Sum ((seq_id x) rto_power p)) to_power (1 / p))
A6:
|.a.| to_power p >= 0
by A1, Lm1, COMPLEX1:46;
thus (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) =
((|.a.| to_power p) * (Sum ((seq_id x) rto_power p))) to_power (1 / p)
by A1, A3, Lm6
.=
((|.a.| to_power p) to_power (1 / p)) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p))
by A2, A5, A6, Lm2
.=
(|.a.| to_power (p * (1 / p))) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p))
by A1, A2, COMPLEX1:46, HOLDER_1:2
.=
(|.a.| to_power 1) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p))
by A1, XCMPLX_1:106
.=
|.a.| * ((Sum ((seq_id x) rto_power p)) to_power (1 / p))
by POWER:25
; verum