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 S1[ 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: S1[ 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
.= 1 by A5
.= ((lim s1) GeoSeq) . 0 by Th3
.= (lim s1) |^ 0 by Def1 ; :: thesis: verum
end;
A7: for m1 being Nat st S1[m1] holds
S1[m1 + 1]
proof
let m1 be Nat; :: thesis: ( S1[m1] implies S1[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: S1[m1 + 1]
deffunc H1( 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 = H1(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 ; :: thesis: lim s = (lim s1) |^ (m1 + 1)
lim s3 = (lim s1) |^ m1 by A8, A9;
hence lim s = ((lim s1) |^ m1) * (lim s1) by
.= (lim s1) |^ (m1 + 1) by NEWTON:6 ;
:: thesis: verum
end;
for m1 being Nat holds S1[m1] from NAT_1:sch 2(A3, A7);
hence ( s2 is convergent & lim s2 = (lim s1) |^ m ) by A2; :: thesis: verum