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₁[ 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₁[ 0 ]

proof

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;

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

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;

then A6: s is constant by VALUED_0:def 18;
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;

A7: for m1 being Nat st S₁[m1] holds
S₁[m1 + 1]

proof

let m1 be Nat; :: thesis: ( S₁[m1] implies S₁[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₁[m1 + 1]
deffunc H₁( 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₁(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) )

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

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;

then A11: s = s3 (#) s1 by SEQ_1:8;
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;

for m1 being Nat holds S₁[m1] from NAT_1:sch 2(A3, A7);
hence ( s2 is convergent & lim s2 = (lim s1) |^ m ) by A2; :: thesis: verum