let p be Real; :: thesis:
assume A1: 0 < p ; :: thesis:
let c be Real; :: thesis:
let seq be Real_Sequence; :: thesis:
assume A2: seq is convergent ; :: thesis:
deffunc H₁( set ) -> object = |.((seq . $1) - c).|;
consider b being Real_Sequence such that
A3: for n being Nat holds b . n = H₁(n) from SEQ_1:sch 1();
let rseq be Real_Sequence; :: thesis:
assume A4: for i being Nat holds rseq . i = |.((seq . i) - c).| to_power p ; :: thesis:
A5: for n being Nat holds rseq . n = (b . n) to_power p

let n be Nat; :: thesis:
rseq . n = |.((seq . n) - c).| to_power p by A4
.= (b . n) to_power p by A3 ;
hence rseq . n = (b . n) to_power p ; :: thesis:

end;

let n be Nat; :: thesis:
b . n = |.((seq . n) - c).| by A3;
hence 0 <= b . n by COMPLEX1:46; :: thesis:

end;