set S = SgmX ((RelIncl n),A);
defpred S₁[ object , object ] means ( $2 is Complex & ( for z being Complex st z = $2 holds
( z ^2 = f . ((SgmX ((RelIncl n),A)) . $1) & Re z >= 0 & Im z >= 0 ) ) );
A1: for i being Nat st i in Seg (len (SgmX ((RelIncl n),A))) holds
ex y being object st S₁[i,y]

proof

let i be Nat; :: thesis: ( i in Seg (len (SgmX ((RelIncl n),A))) implies ex y being object st S₁[i,y] )
assume i in Seg (len (SgmX ((RelIncl n),A))) ; :: thesis: ex y being object st S₁[i,y]
set fS = f . ((SgmX ((RelIncl n),A)) . i);

per cases ( f . ((SgmX ((RelIncl n),A)) . i) >= 0 or f . ((SgmX ((RelIncl n),A)) . i) < 0 ) ;

suppose A2: f . ((SgmX ((RelIncl n),A)) . i) >= 0 ; :: thesis: ex y being object st S₁[i,y]

take z1 = sqrt (f . ((SgmX ((RelIncl n),A)) . i)); :: thesis: S₁[i,z1]
thus z1 is Complex ; :: thesis: for z being Complex st z = z1 holds
( z ^2 = f . ((SgmX ((RelIncl n),A)) . i) & Re z >= 0 & Im z >= 0 )
let z be Complex; :: thesis: ( z = z1 implies ( z ^2 = f . ((SgmX ((RelIncl n),A)) . i) & Re z >= 0 & Im z >= 0 ) )
assume z = z1 ; :: thesis: ( z ^2 = f . ((SgmX ((RelIncl n),A)) . i) & Re z >= 0 & Im z >= 0 )
hence ( z ^2 = f . ((SgmX ((RelIncl n),A)) . i) & Re z >= 0 & Im z >= 0 ) by SQUARE_1:def 2, A2, COMPLEX1:def 2; :: thesis: verum

end;

suppose A3: f . ((SgmX ((RelIncl n),A)) . i) < 0 ; :: thesis: ex y being object st S₁[i,y]

take z1 = (sqrt (- (f . ((SgmX ((RelIncl n),A)) . i)))) * <i>; :: thesis: S₁[i,z1]
thus z1 is Complex ; :: thesis: for z being Complex st z = z1 holds
( z ^2 = f . ((SgmX ((RelIncl n),A)) . i) & Re z >= 0 & Im z >= 0 )
let z be Complex; :: thesis: ( z = z1 implies ( z ^2 = f . ((SgmX ((RelIncl n),A)) . i) & Re z >= 0 & Im z >= 0 ) )
assume A4: z = z1 ; :: thesis: ( z ^2 = f . ((SgmX ((RelIncl n),A)) . i) & Re z >= 0 & Im z >= 0 )
A5: ( sqrt (- (f . ((SgmX ((RelIncl n),A)) . i))) >= 0 & (sqrt (- (f . ((SgmX ((RelIncl n),A)) . i)))) * (sqrt (- (f . ((SgmX ((RelIncl n),A)) . i)))) = (sqrt (- (f . ((SgmX ((RelIncl n),A)) . i)))) ^2 & (sqrt (- (f . ((SgmX ((RelIncl n),A)) . i)))) ^2 = - (f . ((SgmX ((RelIncl n),A)) . i)) ) by SQUARE_1:def 1, SQUARE_1:def 2, A3;
( Re (z1 * z1) = ((Re z1) * (Re z1)) - ((Im z1) * (Im z1)) & Im (z1 * z1) = ((Re z1) * (Im z1)) + ((Re z1) * (Im z1)) ) by COMPLEX1:9;
hence ( z ^2 = f . ((SgmX ((RelIncl n),A)) . i) & Re z >= 0 & Im z >= 0 ) by A4, A5, SQUARE_1:def 1; :: thesis: verum

end;

end;

end;

consider p being FinSequence such that
A7: ( dom p = Seg (len (SgmX ((RelIncl n),A))) & ( for k being Nat st k in Seg (len (SgmX ((RelIncl n),A))) holds
S₁[k,p . k] ) ) from FINSEQ_1:sch 1(A1);
f . x in COMPLEX by XCMPLX_0:def 2;
then reconsider f1 = f . x as Element of F_Complex by COMPLFLD:def 1;
rng p c= the carrier of F_Complex

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in the carrier of F_Complex )
assume A8: y in rng p ; :: thesis: y in the carrier of F_Complex
consider x being object such that
A9: ( x in dom p & p . x = y ) by A8, FUNCT_1:def 3;
S₁[x,p . x] by A9, A7;
then p . x in COMPLEX by XCMPLX_0:def 2;
hence y in the carrier of F_Complex by A9, COMPLFLD:def 1; :: thesis: verum

end;

then reconsider p = p as FinSequence of F_Complex by FINSEQ_1:def 4;
take C = <*f1*> ^ p; :: thesis: ( len C = 1 + (card A) & C . 1 = f . x & ( for i being Nat st i in dom (SgmX ((RelIncl n),A)) holds
( (C . (i + 1)) ^2 = f . ((SgmX ((RelIncl n),A)) . i) & Re (C . (i + 1)) >= 0 & Im (C . (i + 1)) >= 0 ) ) )
A10: len <*f1*> = 1 by FINSEQ_1:39;
( len p = len (SgmX ((RelIncl n),A)) & len (SgmX ((RelIncl n),A)) = card A ) by A7, FINSEQ_1:def 3, Th5, PRE_POLY:11;
hence ( len C = 1 + (card A) & C . 1 = f . x ) by A10, FINSEQ_1:22; :: thesis: for i being Nat st i in dom (SgmX ((RelIncl n),A)) holds
( (C . (i + 1)) ^2 = f . ((SgmX ((RelIncl n),A)) . i) & Re (C . (i + 1)) >= 0 & Im (C . (i + 1)) >= 0 )
let i be Nat; :: thesis: ( i in dom (SgmX ((RelIncl n),A)) implies ( (C . (i + 1)) ^2 = f . ((SgmX ((RelIncl n),A)) . i) & Re (C . (i + 1)) >= 0 & Im (C . (i + 1)) >= 0 ) )
assume A11: i in dom (SgmX ((RelIncl n),A)) ; :: thesis: ( (C . (i + 1)) ^2 = f . ((SgmX ((RelIncl n),A)) . i) & Re (C . (i + 1)) >= 0 & Im (C . (i + 1)) >= 0 )
A12: dom (SgmX ((RelIncl n),A)) = dom p by A7, FINSEQ_1:def 3;
then C . (i + 1) = p . i by A11, A10, FINSEQ_1:def 7;
hence ( (C . (i + 1)) ^2 = f . ((SgmX ((RelIncl n),A)) . i) & Re (C . (i + 1)) >= 0 & Im (C . (i + 1)) >= 0 ) by A7, A11, A12; :: thesis: verum