let p be Real; :: thesis: ( 1 <= p implies for lp being non empty NORMSTR st lp = NORMSTR(# ,,,,() #) holds
for x being Point of lp
for a being Real holds (seq_id (a * x)) rto_power p = () (#) (() rto_power p) )

assume A1: 1 <= p ; :: thesis: for lp being non empty NORMSTR st lp = NORMSTR(# ,,,,() #) holds
for x being Point of lp
for a being Real holds (seq_id (a * x)) rto_power p = () (#) (() rto_power p)

let lp be non empty NORMSTR ; :: thesis: ( lp = NORMSTR(# ,,,,() #) implies for x being Point of lp
for a being Real holds (seq_id (a * x)) rto_power p = () (#) (() rto_power p) )

assume A2: lp = NORMSTR(# ,,,,() #) ; :: thesis: for x being Point of lp
for a being Real holds (seq_id (a * x)) rto_power p = () (#) (() rto_power p)

let x be Point of lp; :: thesis: for a being Real holds (seq_id (a * x)) rto_power p = () (#) (() rto_power p)
let a be Real; :: thesis: (seq_id (a * x)) rto_power p = () (#) (() rto_power p)
now :: thesis: for n1 being object st n1 in NAT holds
((seq_id (a * x)) rto_power p) . n1 = (() (#) (() rto_power p)) . n1
let n1 be object ; :: thesis: ( n1 in NAT implies ((seq_id (a * x)) rto_power p) . n1 = (() (#) (() rto_power p)) . n1 )
assume n1 in NAT ; :: thesis: ((seq_id (a * x)) rto_power p) . n1 = (() (#) (() rto_power p)) . n1
then reconsider n = n1 as Nat ;
A3: |.a.| >= 0 by COMPLEX1:46;
A4: |.(() . 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 (#) ())) . n).| to_power p by A1, A2, Th10
.= |.(a * (() . n)).| to_power p by SEQ_1:9
.= (|.a.| * |.(() . n).|) to_power p by COMPLEX1:65
.= () * (|.(() . n).| to_power p) by A1, A3, A4, Lm2
.= () * ((() rto_power p) . n) by Def1
.= (() (#) (() rto_power p)) . n by SEQ_1:9 ;
hence ((seq_id (a * x)) rto_power p) . n1 = (() (#) (() rto_power p)) . n1 ; :: thesis: verum
end;
hence (seq_id (a * x)) rto_power p = () (#) (() rto_power p) by FUNCT_2:12; :: thesis: verum