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 = (|.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 = (|.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 = (|.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 = (|.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 = (|.a.| to_power p) (#) ((seq_id x) rto_power p)
let a be Real; :: thesis: (seq_id (a * x)) rto_power p = (|.a.| to_power p) (#) ((seq_id x) rto_power p)

now :: thesis: for n1 being object st n1 in NAT holds
((seq_id (a * x)) rto_power p) . n1 = ((|.a.| to_power p) (#) ((seq_id x) rto_power p)) . n1

let n1 be object ; :: thesis: ( n1 in NAT implies ((seq_id (a * x)) rto_power p) . n1 = ((|.a.| to_power p) (#) ((seq_id x) rto_power p)) . n1 )
assume n1 in NAT ; :: thesis: ((seq_id (a * x)) rto_power p) . n1 = ((|.a.| to_power p) (#) ((seq_id x) rto_power p)) . n1
then reconsider n = n1 as Nat ;
A3: |.a.| >= 0 by COMPLEX1:46;
A4: |.((seq_id x) . n).| >= 0 by COMPLEX1:46;
((seq_id (a * x)) rto_power p) . n = |.((seq_id (a * x)) . n).| to_power p by Def1
.= |.((seq_id (a (#) (seq_id x))) . n).| to_power p by A1, A2, Th10
.= |.(a * ((seq_id x) . n)).| to_power p by SEQ_1:9
.= (|.a.| * |.((seq_id x) . n).|) to_power p by COMPLEX1:65
.= (|.a.| to_power p) * (|.((seq_id x) . n).| to_power p) by A1, A3, A4, Lm2
.= (|.a.| to_power p) * (((seq_id x) rto_power p) . n) by Def1
.= ((|.a.| to_power p) (#) ((seq_id x) rto_power p)) . n by SEQ_1:9 ;
hence ((seq_id (a * x)) rto_power p) . n1 = ((|.a.| to_power p) (#) ((seq_id x) rto_power p)) . n1 ; :: thesis: verum

end;

hence (seq_id (a * x)) rto_power p = (|.a.| to_power p) (#) ((seq_id x) rto_power p) by FUNCT_2:12; :: thesis: verum