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 (seq_id (a * x)) rto_power p = ((abs a) to_power p) (#) ((seq_id x) rto_power 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 (seq_id (a * x)) rto_power p = ((abs a) to_power p) (#) ((seq_id x) rto_power 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 (seq_id (a * x)) rto_power p = ((abs 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) #) ; :: thesis: for x being Point of lp
for a being Real holds (seq_id (a * x)) rto_power p = ((abs a) to_power p) (#) ((seq_id x) rto_power p)
let x be Point of lp; :: thesis: for a being Real holds (seq_id (a * x)) rto_power p = ((abs a) to_power p) (#) ((seq_id x) rto_power p)
let a be Real; :: thesis: (seq_id (a * x)) rto_power p = ((abs a) to_power p) (#) ((seq_id x) rto_power p)

now

let n1 be set ; :: thesis: ( n1 in NAT implies ((seq_id (a * x)) rto_power p) . n1 = (((abs a) to_power p) (#) ((seq_id x) rto_power p)) . n1 )
assume A3: n1 in NAT ; :: thesis: ((seq_id (a * x)) rto_power p) . n1 = (((abs a) to_power p) (#) ((seq_id x) rto_power p)) . n1
reconsider n = n1 as Element of NAT by A3;
A4: ( abs a >= 0 & abs ((seq_id x) . n) >= 0 ) by COMPLEX1:132;
A5: ((seq_id (a * x)) rto_power p) . n = (abs ((seq_id (a * x)) . n)) to_power p by Def1
.= (abs ((seq_id (a (#) (seq_id x))) . n)) to_power p by A1, A2, Th10
.= (abs ((a (#) (seq_id x)) . n)) to_power p by RSSPACE:3
.= (abs (a * ((seq_id x) . n))) to_power p by SEQ_1:13
.= ((abs a) * (abs ((seq_id x) . n))) to_power p by COMPLEX1:151
.= ((abs a) to_power p) * ((abs ((seq_id x) . n)) to_power p) by A1, A4, Lm2
.= ((abs a) to_power p) * (((seq_id x) rto_power p) . n) by Def1
.= (((abs a) to_power p) (#) ((seq_id x) rto_power p)) . n by SEQ_1:13 ;
thus ((seq_id (a * x)) rto_power p) . n1 = (((abs a) to_power p) (#) ((seq_id x) rto_power p)) . n1 by A5; :: thesis: verum

end;

hence (seq_id (a * x)) rto_power p = ((abs a) to_power p) (#) ((seq_id x) rto_power p) by FUNCT_2:18; :: thesis: verum