let seq be positive-yielding Real_Sequence; :: thesis: ( seq is convergent implies ( sqrt seq is convergent & lim (sqrt seq) = sqrt (lim seq) ) )
assume A1: seq is convergent ; :: thesis: ( sqrt seq is convergent & lim (sqrt seq) = sqrt (lim seq) )
then consider a being Real such that
A2: for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - a).| < r ;
A3: for k being Nat holds seq . k >= 0 ;
A4: a = lim seq by A1, A2, SEQ_2:def 7;
A5: for k being Nat holds sqrt (seq . k) = (sqrt seq) . k

proof

let k be Nat; :: thesis: sqrt (seq . k) = (sqrt seq) . k
dom (sqrt seq) = NAT by FUNCT_2:def 1;
hence sqrt (seq . k) = (sqrt seq) . k by PARTFUN3:def 5, ORDINAL1:def 12; :: thesis: verum

end;

( sqrt seq is convergent & lim (sqrt seq) = sqrt (lim seq) )

proof

for r1 being Real st 0 < r1 holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((sqrt seq) . m) - (sqrt a)).| < r1

proof

let r1 be Real; :: thesis: ( 0 < r1 implies ex n being Nat st
for m being Nat st n <= m holds
|.(((sqrt seq) . m) - (sqrt a)).| < r1 )
assume A7: 0 < r1 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((sqrt seq) . m) - (sqrt a)).| < r1

per cases ( a = 0 or a > 0 ) by A1, A3, A4, SEQ_2:17;

suppose A8: a = 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((sqrt seq) . m) - (sqrt a)).| < r1

consider n0 being Nat such that
A9: for k being Nat st n0 <= k holds
|.((seq . k) - a).| < r1 ^2 by A2, A7;
for m being Nat st n0 <= m holds
|.(((sqrt seq) . m) - (sqrt a)).| < r1

proof

let m be Nat; :: thesis: ( n0 <= m implies |.(((sqrt seq) . m) - (sqrt a)).| < r1 )
assume A10: n0 <= m ; :: thesis: |.(((sqrt seq) . m) - (sqrt a)).| < r1
A11: ( seq . m > 0 & (sqrt seq) . m = sqrt (seq . m) ) by Lm11, A5;
|.((seq . m) - a).| = seq . m by A8;
then seq . m < r1 ^2 by A9, A10;
then (sqrt seq) . m < sqrt (r1 ^2) by A11, SQUARE_1:27;
hence |.(((sqrt seq) . m) - (sqrt a)).| < r1 by A8, A7, SQUARE_1:22; :: thesis: verum

end;

hence ex n being Nat st
for m being Nat st n <= m holds
|.(((sqrt seq) . m) - (sqrt a)).| < r1 ; :: thesis: verum

end;

suppose A14: a > 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((sqrt seq) . m) - (sqrt a)).| < r1

reconsider sqa = sqrt a as Real ;
consider n0 being Nat such that
A15: for k being Nat st n0 <= k holds
|.((seq . k) - a).| < sqa * r1 by A2, A14, A7;
for m being Nat st n0 <= m holds
|.(((sqrt seq) . m) - (sqrt a)).| < r1

proof

let m be Nat; :: thesis: ( n0 <= m implies |.(((sqrt seq) . m) - (sqrt a)).| < r1 )
assume n0 <= m ; :: thesis: |.(((sqrt seq) . m) - (sqrt a)).| < r1
then A18: |.((seq . m) - a).| < sqa * r1 by A15;
set sqs1 = (sqrt seq) . m;
A17: ( seq . m > 0 & (sqrt seq) . m = sqrt (seq . m) ) by Lm11, A5;
A19: sqrt a < ((sqrt seq) . m) + (sqrt a) by Lm11, XREAL_1:29;
A20: |.sqa.| = sqa by A14, COMPLEX1:43;
then A21: |.(sqrt a).| < |.(((sqrt seq) . m) + (sqrt a)).| by A19, A14, COMPLEX1:43;
((seq . m) - a) / (((sqrt seq) . m) + sqa) = ((((sqrt seq) . m) - sqa) * (((sqrt seq) . m) + sqa)) * (1 / (((sqrt seq) . m) + sqa)) by A17, A14, SQUARE_1:35
.= ((sqrt seq) . m) - sqa by A14, XCMPLX_1:107 ;
then A22: |.(((sqrt seq) . m) - sqa).| = |.((seq . m) - a).| / |.(((sqrt seq) . m) + sqa).| by COMPLEX1:67;
0 <= |.((seq . m) - a).| by COMPLEX1:46;
then A23: |.((seq . m) - a).| / |.(((sqrt seq) . m) + sqa).| <= |.((seq . m) - a).| / |.sqa.| by XREAL_1:118, A14, A21;
A24: (sqa * r1) / sqa = r1 by A14, XCMPLX_1:89;
|.((seq . m) - a).| / |.sqa.| < (sqa * r1) / sqa by A14, A18, A20, XREAL_1:74;
hence |.(((sqrt seq) . m) - (sqrt a)).| < r1 by A22, A24, A23, XXREAL_0:2; :: thesis: verum

end;

hence ex n being Nat st
for m being Nat st n <= m holds
|.(((sqrt seq) . m) - (sqrt a)).| < r1 ; :: thesis: verum

end;

end;

end;

then consider x being Real such that
A26: x = sqrt a and
A27: for r1 being Real st 0 < r1 holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((sqrt seq) . m) - x).| < r1 ;
sqrt seq is convergent by A27;
then lim (sqrt seq) = sqrt a by A26, A27, SEQ_2:def 7
.= sqrt (lim seq) by A1, A2, SEQ_2:def 7 ;
hence ( sqrt seq is convergent & lim (sqrt seq) = sqrt (lim seq) ) by A27; :: thesis: verum

end;

hence ( sqrt seq is convergent & lim (sqrt seq) = sqrt (lim seq) ) ; :: thesis: verum