let seq1, seq2 be Real_Sequence; :: thesis: for k being positive Real st ( for n being Nat holds

( seq1 . n = (seq2 . n) to_power k & seq2 . n >= 0 ) ) holds

( seq1 is convergent iff seq2 is convergent )

let k be positive Real; :: thesis: ( ( for n being Nat holds

( seq1 . n = (seq2 . n) to_power k & seq2 . n >= 0 ) ) implies ( seq1 is convergent iff seq2 is convergent ) )

assume A1: for n being Nat holds

( seq1 . n = (seq2 . n) to_power k & seq2 . n >= 0 ) ; :: thesis: ( seq1 is convergent iff seq2 is convergent )

A2: for n being Nat holds seq1 . n >= 0

hence seq1 is convergent by A1, HOLDER_1:10; :: thesis: verum

( seq1 . n = (seq2 . n) to_power k & seq2 . n >= 0 ) ) holds

( seq1 is convergent iff seq2 is convergent )

let k be positive Real; :: thesis: ( ( for n being Nat holds

( seq1 . n = (seq2 . n) to_power k & seq2 . n >= 0 ) ) implies ( seq1 is convergent iff seq2 is convergent ) )

assume A1: for n being Nat holds

( seq1 . n = (seq2 . n) to_power k & seq2 . n >= 0 ) ; :: thesis: ( seq1 is convergent iff seq2 is convergent )

A2: for n being Nat holds seq1 . n >= 0

proof

thus
( seq1 is convergent implies seq2 is convergent )
:: thesis: ( seq2 is convergent implies seq1 is convergent )
let n be Nat; :: thesis: seq1 . n >= 0

(seq2 . n) to_power k >= 0 by A1, Th4;

hence seq1 . n >= 0 by A1; :: thesis: verum

end;(seq2 . n) to_power k >= 0 by A1, Th4;

hence seq1 . n >= 0 by A1; :: thesis: verum

proof

assume
seq2 is convergent
; :: thesis: seq1 is convergent
assume A3:
seq1 is convergent
; :: thesis: seq2 is convergent

for n being Nat holds seq2 . n = (seq1 . n) to_power (1 / k)

end;for n being Nat holds seq2 . n = (seq1 . n) to_power (1 / k)

proof

hence
seq2 is convergent
by A2, A3, HOLDER_1:10; :: thesis: verum
let n be Nat; :: thesis: seq2 . n = (seq1 . n) to_power (1 / k)

(seq1 . n) to_power (1 / k) = ((seq2 . n) to_power k) to_power (1 / k) by A1

.= (seq2 . n) to_power (k * (1 / k)) by A1, HOLDER_1:2

.= (seq2 . n) to_power 1 by XCMPLX_1:106 ;

hence seq2 . n = (seq1 . n) to_power (1 / k) by POWER:25; :: thesis: verum

end;(seq1 . n) to_power (1 / k) = ((seq2 . n) to_power k) to_power (1 / k) by A1

.= (seq2 . n) to_power (k * (1 / k)) by A1, HOLDER_1:2

.= (seq2 . n) to_power 1 by XCMPLX_1:106 ;

hence seq2 . n = (seq1 . n) to_power (1 / k) by POWER:25; :: thesis: verum

hence seq1 is convergent by A1, HOLDER_1:10; :: thesis: verum