let C1, C2 be FinSequence of F_Complex; :: thesis: ( len C1 = len f & C1 . 1 = f . 1 & ( for i being Nat st i in dom f & i <> 1 holds
( (C1 . i) ^2 = f . i & Re (C1 . i) >= 0 & Im (C1 . i) >= 0 ) ) & len C2 = len f & C2 . 1 = f . 1 & ( for i being Nat st i in dom f & i <> 1 holds
( (C2 . i) ^2 = f . i & Re (C2 . i) >= 0 & Im (C2 . i) >= 0 ) ) implies C1 = C2 )
assume that
A14: ( len C1 = len f & C1 . 1 = f . 1 ) and
A15: for i being Nat st i in dom f & i <> 1 holds
( (C1 . i) ^2 = f . i & Re (C1 . i) >= 0 & Im (C1 . i) >= 0 ) and
A16: ( len C2 = len f & C2 . 1 = f . 1 ) and
A17: for i being Nat st i in dom f & i <> 1 holds
( (C2 . i) ^2 = f . i & Re (C2 . i) >= 0 & Im (C2 . i) >= 0 ) ; :: thesis: C1 = C2
for i being Nat st 1 <= i & i <= len C1 holds
C1 . i = C2 . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len C1 implies C1 . i = C2 . i )
assume A18: ( 1 <= i & i <= len C1 ) ; :: thesis: C1 . i = C2 . i

per cases ( i = 1 or i > 1 ) by A18, XXREAL_0:1;

suppose i = 1 ; :: thesis: C1 . i = C2 . i

hence C1 . i = C2 . i by A14, A16; :: thesis: verum

end;

suppose A19: i > 1 ; :: thesis: C1 . i = C2 . i

i in dom f by A18, A14, FINSEQ_3:25;
then ( (C1 . i) ^2 = f . i & Re (C1 . i) >= 0 & Im (C1 . i) >= 0 & (C2 . i) ^2 = f . i & Re (C2 . i) >= 0 & Im (C2 . i) >= 0 ) by A19, A17, A15;
hence C1 . i = C2 . i by Th2; :: thesis: verum

end;

end;

end;

hence C1 = C2 by A14, A16, FINSEQ_1:14; :: thesis: verum