let seq1, seq2 be Real_Sequence; :: thesis: for k being positive Real st ( for n being Element of 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 Element of NAT holds
( seq1 . n = (seq2 . n) to_power k & seq2 . n >= 0 ) ) implies ( seq1 is convergent iff seq2 is convergent ) )
assume AS: for n being Element of NAT holds
( seq1 . n = (seq2 . n) to_power k & seq2 . n >= 0 ) ; :: thesis: ( seq1 is convergent iff seq2 is convergent )
A1: for n being Element of NAT holds seq1 . n >= 0

proof

let n be Element of NAT ; :: thesis: seq1 . n >= 0
(seq2 . n) to_power k >= 0 by AS, LmPW001;
hence seq1 . n >= 0 by AS; :: thesis: verum

end;

thus ( seq1 is convergent implies seq2 is convergent ) :: thesis: ( seq2 is convergent implies seq1 is convergent )

proof

assume A2: seq1 is convergent ; :: thesis: seq2 is convergent
for n being Element of NAT holds seq2 . n = (seq1 . n) to_power (1 / k)

proof

let n be Element of 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 AS
.= (seq2 . n) to_power (k * (1 / k)) by AS, HOLDER_1:2
.= (seq2 . n) to_power 1 by XCMPLX_1:107 ;
hence seq2 . n = (seq1 . n) to_power (1 / k) by POWER:30; :: thesis: verum

end;

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

end;

assume seq2 is convergent ; :: thesis: seq1 is convergent
hence seq1 is convergent by AS, HOLDER_1:10; :: thesis: verum