theorem Th71: :: POLYNOM9:71

for i being Nat
for f being real-valued FinSequence st i > 1 & f . i >= 0 holds
(_sqrt f) . i = sqrt (f . i)