:: deftheorem defines _sqrtSegm POLYNOM9:def 7 :
for n being Ordinal
for x being object
for A being finite Subset of n
for f being real-valued Function
for b₅ being FinSequence of F_Complex holds
( b₅ = _sqrtSegm (f,x,A) iff ( len b₅ = 1 + (card A) & b₅ . 1 = f . x & ( for i being Nat st i in dom (SgmX ((RelIncl n),A)) holds
( (b₅ . (i + 1)) ^2 = f . ((SgmX ((RelIncl n),A)) . i) & Re (b₅ . (i + 1)) >= 0 & Im (b₅ . (i + 1)) >= 0 ) ) ) );