let m be Nat; :: thesis: for s1, s2 being Real_Sequence st s1 is convergent & ( for n being Nat holds s2 . n = (s1 . n) |^ m ) holds

( s2 is convergent & lim s2 = (lim s1) |^ m )

let s1, s2 be Real_Sequence; :: thesis: ( s1 is convergent & ( for n being Nat holds s2 . n = (s1 . n) |^ m ) implies ( s2 is convergent & lim s2 = (lim s1) |^ m ) )

assume that

A1: s1 is convergent and

A2: for n being Nat holds s2 . n = (s1 . n) |^ m ; :: thesis: ( s2 is convergent & lim s2 = (lim s1) |^ m )

defpred S_{1}[ Nat] means for s being Real_Sequence st ( for n being Nat holds s . n = (s1 . n) |^ $1 ) holds

( s is convergent & lim s = (lim s1) |^ $1 );

A3: S_{1}[ 0 ]
_{1}[m1] holds

S_{1}[m1 + 1]
_{1}[m1]
from NAT_1:sch 2(A3, A7);

hence ( s2 is convergent & lim s2 = (lim s1) |^ m ) by A2; :: thesis: verum

( s2 is convergent & lim s2 = (lim s1) |^ m )

let s1, s2 be Real_Sequence; :: thesis: ( s1 is convergent & ( for n being Nat holds s2 . n = (s1 . n) |^ m ) implies ( s2 is convergent & lim s2 = (lim s1) |^ m ) )

assume that

A1: s1 is convergent and

A2: for n being Nat holds s2 . n = (s1 . n) |^ m ; :: thesis: ( s2 is convergent & lim s2 = (lim s1) |^ m )

defpred S

( s is convergent & lim s = (lim s1) |^ $1 );

A3: S

proof

A7:
for m1 being Nat st S
let s be Real_Sequence; :: thesis: ( ( for n being Nat holds s . n = (s1 . n) |^ 0 ) implies ( s is convergent & lim s = (lim s1) |^ 0 ) )

assume A4: for n being Nat holds s . n = (s1 . n) |^ 0 ; :: thesis: ( s is convergent & lim s = (lim s1) |^ 0 )

reconsider j = 1 as Element of REAL by NUMBERS:19;

hence s is convergent ; :: thesis: lim s = (lim s1) |^ 0

thus lim s = s . 0 by A6, SEQ_4:26

.= 1 by A5

.= ((lim s1) GeoSeq) . 0 by Th3

.= (lim s1) |^ 0 by Def1 ; :: thesis: verum

end;assume A4: for n being Nat holds s . n = (s1 . n) |^ 0 ; :: thesis: ( s is convergent & lim s = (lim s1) |^ 0 )

reconsider j = 1 as Element of REAL by NUMBERS:19;

A5: now :: thesis: for n being Nat holds s . n = j

then A6:
s is constant
by VALUED_0:def 18;let n be Nat; :: thesis: s . n = j

thus s . n = (s1 . n) |^ 0 by A4

.= ((s1 . n) GeoSeq) . 0 by Def1

.= j by Th3 ; :: thesis: verum

end;thus s . n = (s1 . n) |^ 0 by A4

.= ((s1 . n) GeoSeq) . 0 by Def1

.= j by Th3 ; :: thesis: verum

hence s is convergent ; :: thesis: lim s = (lim s1) |^ 0

thus lim s = s . 0 by A6, SEQ_4:26

.= 1 by A5

.= ((lim s1) GeoSeq) . 0 by Th3

.= (lim s1) |^ 0 by Def1 ; :: thesis: verum

S

proof

for m1 being Nat holds S
let m1 be Nat; :: thesis: ( S_{1}[m1] implies S_{1}[m1 + 1] )

assume A8: for s being Real_Sequence st ( for n being Nat holds s . n = (s1 . n) |^ m1 ) holds

( s is convergent & lim s = (lim s1) |^ m1 ) ; :: thesis: S_{1}[m1 + 1]

deffunc H_{1}( Nat) -> set = (s1 . $1) |^ m1;

let s be Real_Sequence; :: thesis: ( ( for n being Nat holds s . n = (s1 . n) |^ (m1 + 1) ) implies ( s is convergent & lim s = (lim s1) |^ (m1 + 1) ) )

consider s3 being Real_Sequence such that

A9: for n being Nat holds s3 . n = H_{1}(n)
from SEQ_1:sch 1();

assume A10: for n being Nat holds s . n = (s1 . n) |^ (m1 + 1) ; :: thesis: ( s is convergent & lim s = (lim s1) |^ (m1 + 1) )

A12: s3 is convergent by A8, A9;

hence s is convergent by A1, A11; :: thesis: lim s = (lim s1) |^ (m1 + 1)

lim s3 = (lim s1) |^ m1 by A8, A9;

hence lim s = ((lim s1) |^ m1) * (lim s1) by A1, A12, A11, SEQ_2:15

.= (lim s1) |^ (m1 + 1) by NEWTON:6 ;

:: thesis: verum

end;assume A8: for s being Real_Sequence st ( for n being Nat holds s . n = (s1 . n) |^ m1 ) holds

( s is convergent & lim s = (lim s1) |^ m1 ) ; :: thesis: S

deffunc H

let s be Real_Sequence; :: thesis: ( ( for n being Nat holds s . n = (s1 . n) |^ (m1 + 1) ) implies ( s is convergent & lim s = (lim s1) |^ (m1 + 1) ) )

consider s3 being Real_Sequence such that

A9: for n being Nat holds s3 . n = H

assume A10: for n being Nat holds s . n = (s1 . n) |^ (m1 + 1) ; :: thesis: ( s is convergent & lim s = (lim s1) |^ (m1 + 1) )

now :: thesis: for n being Nat holds s . n = (s3 . n) * (s1 . n)

then A11:
s = s3 (#) s1
by SEQ_1:8;let n be Nat; :: thesis: s . n = (s3 . n) * (s1 . n)

thus s . n = (s1 . n) |^ (m1 + 1) by A10

.= ((s1 . n) |^ m1) * (s1 . n) by NEWTON:6

.= (s3 . n) * (s1 . n) by A9 ; :: thesis: verum

end;thus s . n = (s1 . n) |^ (m1 + 1) by A10

.= ((s1 . n) |^ m1) * (s1 . n) by NEWTON:6

.= (s3 . n) * (s1 . n) by A9 ; :: thesis: verum

A12: s3 is convergent by A8, A9;

hence s is convergent by A1, A11; :: thesis: lim s = (lim s1) |^ (m1 + 1)

lim s3 = (lim s1) |^ m1 by A8, A9;

hence lim s = ((lim s1) |^ m1) * (lim s1) by A1, A12, A11, SEQ_2:15

.= (lim s1) |^ (m1 + 1) by NEWTON:6 ;

:: thesis: verum

hence ( s2 is convergent & lim s2 = (lim s1) |^ m ) by A2; :: thesis: verum