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 (seq_id (a * x)) rto_power p = (|.a.| to_power p) (#) ((seq_id x) rto_power 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 (seq_id (a * x)) rto_power p = (|.a.| to_power p) (#) ((seq_id x) rto_power p)
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 (seq_id (a * x)) rto_power p = (|.a.| to_power p) (#) ((seq_id x) rto_power 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) #)
; for x being Point of lp
for a being Real holds (seq_id (a * x)) rto_power p = (|.a.| to_power p) (#) ((seq_id x) rto_power p)
let x be Point of lp; for a being Real holds (seq_id (a * x)) rto_power p = (|.a.| to_power p) (#) ((seq_id x) rto_power p)
let a be Real; (seq_id (a * x)) rto_power p = (|.a.| to_power p) (#) ((seq_id x) rto_power p)
hence
(seq_id (a * x)) rto_power p = (|.a.| to_power p) (#) ((seq_id x) rto_power p)
by FUNCT_2:12; verum