let s be Real_Sequence; :: thesis: for a being real number st a > 0 & ( for n being Element of NAT st n >= 1 holds
s . n = n -root a ) holds
( s is convergent & lim s = 1 )
let a be real number ; :: thesis: ( a > 0 & ( for n being Element of 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 Element of NAT st n >= 1 holds
s . n = n -root a ; :: thesis: ( s is convergent & lim s = 1 )

A3: now

let n be Element of NAT ; :: thesis: ( n >= 1 implies s . n = n -Root a )
assume A4: n >= 1 ; :: thesis: s . n = n -Root a
thus s . n = n -root a by A2, A4
.= n -Root a by A1, A4, Def1 ; :: thesis: verum

end;

thus ( s is convergent & lim s = 1 ) by A1, A3, PREPOWER:42; :: thesis: verum