let s be Real_Sequence; :: thesis: for a being Real st a > 0 & ( for n being Nat st n >= 1 holds
s . n = n -root a ) holds
( s is convergent & lim s = 1 )
let a be Real; :: thesis: ( a > 0 & ( for n being Nat st n >= 1 holds
s . n = n -root a ) implies ( s is convergent & lim s = 1 ) )
assume that
A1: a > 0 and
A2: for n being Nat st n >= 1 holds
s . n = n -root a ; :: thesis: ( s is convergent & lim s = 1 )

now :: thesis: for n being Nat st n >= 1 holds
s . n = n -Root a

let n be Nat; :: thesis: ( n >= 1 implies s . n = n -Root a )
assume A3: n >= 1 ; :: thesis: s . n = n -Root a
hence s . n = n -root a by A2
.= n -Root a by A1, A3, Def1 ;
:: thesis: verum

end;

hence ( s is convergent & lim s = 1 ) by A1, PREPOWER:33; :: thesis: verum