let i be Nat; :: thesis: for f being real-valued FinSequence st i > 1 & f . i >= 0 holds
(_sqrt f) . i = sqrt (f . i)
let f be real-valued FinSequence; :: thesis: ( i > 1 & f . i >= 0 implies (_sqrt f) . i = sqrt (f . i) )
assume A1: ( i > 1 & f . i >= 0 ) ; :: thesis: (_sqrt f) . i = sqrt (f . i)
set c = _sqrt f;
len (_sqrt f) = len f by Def11;
then A2: dom (_sqrt f) = dom f by FINSEQ_3:29;

per cases ( not i in dom f or i in dom f ) ;

suppose not i in dom f ; :: thesis: (_sqrt f) . i = sqrt (f . i)

then ( (_sqrt f) . i = 0 & f . i = 0 ) by A2, FUNCT_1:def 2;
hence (_sqrt f) . i = sqrt (f . i) ; :: thesis: verum

end;

suppose i in dom f ; :: thesis: (_sqrt f) . i = sqrt (f . i)

then A3: ( ((_sqrt f) . i) ^2 = f . i & Re ((_sqrt f) . i) >= 0 & Im ((_sqrt f) . i) >= 0 ) by Def11, A1;
A4: sqrt (f . i) >= 0 by A1, SQUARE_1:def 2;
A5: ( Re (sqrt (f . i)) = sqrt (f . i) & Im (sqrt (f . i)) = 0 ) by COMPLEX1:def 2;
(sqrt (f . i)) ^2 = f . i by A1, SQUARE_1:def 2;
hence (_sqrt f) . i = sqrt (f . i) by A3, A5, Th2, A4; :: thesis: verum

end;

end;