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

proof

let i be Nat; :: thesis: ( i in Seg (len f) implies ex y being object st S₁[i,y] )
assume i in Seg (len f) ; :: thesis: ex y being object st S₁[i,y]

per cases ( i = 1 or i <> 1 ) ;

suppose A2: i = 1 ; :: thesis: ex y being object st S₁[i,y]

take F = f . 1; :: thesis: S₁[i,F]
thus S₁[i,F] by A2; :: thesis: verum

end;

suppose A3: i <> 1 ; :: thesis: ex y being object st S₁[i,y]

per cases ( f . i >= 0 or f . i < 0 ) ;

suppose A4: f . i >= 0 ; :: thesis: ex y being object st S₁[i,y]

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

end;

suppose A5: f . i < 0 ; :: thesis: ex y being object st S₁[i,y]

take z1 = (sqrt (- (f . i))) * <i>; :: thesis: S₁[i,z1]
thus ( z1 is Complex & ( i = 1 implies z1 = f . 1 ) ) by A3; :: thesis: ( i <> 1 implies for z being Complex st z = z1 holds
( z ^2 = f . i & Re z >= 0 & Im z >= 0 ) )
assume i <> 1 ; :: thesis: for z being Complex st z = z1 holds
( z ^2 = f . i & Re z >= 0 & Im z >= 0 )
let z be Complex; :: thesis: ( z = z1 implies ( z ^2 = f . i & Re z >= 0 & Im z >= 0 ) )
assume A6: z = z1 ; :: thesis: ( z ^2 = f . i & Re z >= 0 & Im z >= 0 )
A7: ( sqrt (- (f . i)) >= 0 & (sqrt (- (f . i))) * (sqrt (- (f . i))) = (sqrt (- (f . i))) ^2 & (sqrt (- (f . i))) ^2 = - (f . i) ) by SQUARE_1:def 1, SQUARE_1:def 2, A5;
( 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 . i & Re z >= 0 & Im z >= 0 ) by A6, A7, SQUARE_1:def 1; :: thesis: verum

end;

end;

end;

end;

end;

consider p being FinSequence such that
A9: ( dom p = Seg (len f) & ( for k being Nat st k in Seg (len f) holds
S₁[k,p . k] ) ) from FINSEQ_1:sch 1(A1);
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 A10: y in rng p ; :: thesis: y in the carrier of F_Complex
consider x being object such that
A11: ( x in dom p & p . x = y ) by A10, FUNCT_1:def 3;
S₁[x,p . x] by A11, A9;
then p . x in COMPLEX by XCMPLX_0:def 2;
hence y in the carrier of F_Complex by A11, COMPLFLD:def 1; :: thesis: verum

end;

then reconsider p = p as FinSequence of F_Complex by FINSEQ_1:def 4;
take p ; :: thesis: ( len p = len f & p . 1 = f . 1 & ( for i being Nat st i in dom f & i <> 1 holds
( (p . i) ^2 = f . i & Re (p . i) >= 0 & Im (p . i) >= 0 ) ) )
thus len p = len f by A9, FINSEQ_1:def 3; :: thesis: ( p . 1 = f . 1 & ( for i being Nat st i in dom f & i <> 1 holds
( (p . i) ^2 = f . i & Re (p . i) >= 0 & Im (p . i) >= 0 ) ) )
A12: dom p = dom f by A9, FINSEQ_1:def 3;
thus p . 1 = f . 1 :: thesis: for i being Nat st i in dom f & i <> 1 holds
( (p . i) ^2 = f . i & Re (p . i) >= 0 & Im (p . i) >= 0 )

proof

per cases ( 1 in dom p or not 1 in dom p ) ;

suppose 1 in dom p ; :: thesis: p . 1 = f . 1

hence p . 1 = f . 1 by A9; :: thesis: verum

end;

suppose A13: not 1 in dom p ; :: thesis: p . 1 = f . 1

hence p . 1 = 0 by FUNCT_1:def 2
.= f . 1 by A13, A12, FUNCT_1:def 2 ;
:: thesis: verum

end;

end;

end;

let i be Nat; :: thesis: ( i in dom f & i <> 1 implies ( (p . i) ^2 = f . i & Re (p . i) >= 0 & Im (p . i) >= 0 ) )
thus ( i in dom f & i <> 1 implies ( (p . i) ^2 = f . i & Re (p . i) >= 0 & Im (p . i) >= 0 ) ) by A12, A9; :: thesis: verum