let m be Element of NAT ; :: thesis: for s1, s2 being Real_Sequence st s1 is convergent & ( for n being Element of 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 Element of 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 Element of NAT holds s2 . n = (s1 . n) |^ m ; :: thesis: ( s2 is convergent & lim s2 = (lim s1) |^ m )
defpred S₁[ Element of NAT ] means for s being Real_Sequence st ( for n being Element of 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 Element of NAT holds s . n = (s1 . n) |^ 0 ) implies ( s is convergent & lim s = (lim s1) |^ 0 ) )
assume A4: for n being Element of NAT holds s . n = (s1 . n) |^ 0 ; :: thesis: ( s is convergent & lim s = (lim s1) |^ 0 )

A5: now

let n be Nat; :: thesis: s . n = 1
n in NAT by ORDINAL1:def 13;
hence s . n = (s1 . n) |^ 0 by A4
.= ((s1 . n) GeoSeq ) . 0 by Def1
.= 1 by Th4 ;
:: 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:41
.= 1 by A5
.= ((lim s1) GeoSeq ) . 0 by Th4
.= (lim s1) |^ 0 by Def1 ; :: thesis: verum

end;

A7: for m1 being Element of NAT st S₁[m1] holds
S₁[m1 + 1]

proof

let m1 be Element of NAT ; :: thesis: ( S₁[m1] implies S₁[m1 + 1] )
assume A8: for s being Real_Sequence st ( for n being Element of NAT holds s . n = (s1 . n) |^ m1 ) holds
( s is convergent & lim s = (lim s1) |^ m1 ) ; :: thesis: S₁[m1 + 1]
deffunc H₁( Element of NAT ) -> Element of REAL = (s1 . $1) |^ m1;
let s be Real_Sequence; :: thesis: ( ( for n being Element of 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 Element of NAT holds s3 . n = H₁(n) from SEQ_1:sch 1();
assume A10: for n being Element of NAT holds s . n = (s1 . n) |^ (m1 + 1) ; :: thesis: ( s is convergent & lim s = (lim s1) |^ (m1 + 1) )

now

let n be Element of NAT ; :: thesis: s . n = (s3 . n) * (s1 . n)
thus s . n = (s1 . n) |^ (m1 + 1) by A10
.= ((s1 . n) |^ m1) * (s1 . n) by NEWTON:11
.= (s3 . n) * (s1 . n) by A9 ; :: thesis: verum

end;

then A11: s = s3 (#) s1 by SEQ_1:12;
A12: s3 is convergent by A8, A9;
hence s is convergent by A1, A11, SEQ_2:28; :: 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:29
.= (lim s1) |^ (m1 + 1) by NEWTON:11 ;
:: thesis: verum

end;

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