:: deftheorem Def11 defines _sqrt POLYNOM9:def 11 :
for f being real-valued FinSequence
for b₂ being FinSequence of F_Complex holds
( b₂ = _sqrt f iff ( len b₂ = len f & b₂ . 1 = f . 1 & ( for i being Nat st i in dom f & i <> 1 holds
( (b₂ . i) ^2 = f . i & Re (b₂ . i) >= 0 & Im (b₂ . i) >= 0 ) ) ) );