set S = SgmX ((RelIncl n),A);
let C1, C2 be FinSequence of F_Complex; :: thesis: ( len C1 = 1 + (card A) & C1 . 1 = f . x & ( for i being Nat st i in dom (SgmX ((RelIncl n),A)) holds
( (C1 . (i + 1)) ^2 = f . ((SgmX ((RelIncl n),A)) . i) & Re (C1 . (i + 1)) >= 0 & Im (C1 . (i + 1)) >= 0 ) ) & len C2 = 1 + (card A) & C2 . 1 = f . x & ( for i being Nat st i in dom (SgmX ((RelIncl n),A)) holds
( (C2 . (i + 1)) ^2 = f . ((SgmX ((RelIncl n),A)) . i) & Re (C2 . (i + 1)) >= 0 & Im (C2 . (i + 1)) >= 0 ) ) implies C1 = C2 )
assume that
A13: ( len C1 = 1 + (card A) & C1 . 1 = f . x ) and
A14: for i being Nat st i in dom (SgmX ((RelIncl n),A)) holds
( (C1 . (i + 1)) ^2 = f . ((SgmX ((RelIncl n),A)) . i) & Re (C1 . (i + 1)) >= 0 & Im (C1 . (i + 1)) >= 0 ) and
A15: ( len C2 = 1 + (card A) & C2 . 1 = f . x ) and
A16: for i being Nat st i in dom (SgmX ((RelIncl n),A)) holds
( (C2 . (i + 1)) ^2 = f . ((SgmX ((RelIncl n),A)) . i) & Re (C2 . (i + 1)) >= 0 & Im (C2 . (i + 1)) >= 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 A17: ( 1 <= i & i <= len C1 ) ; :: thesis: C1 . i = C2 . i
A18: len (SgmX ((RelIncl n),A)) = card A by Th5, PRE_POLY:11;

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

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

hence C1 . i = C2 . i by A13, A15; :: thesis: verum

end;

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

then reconsider i1 = i - 1 as Nat ;
( 0 <> i1 & i1 <= (len C1) - 1 ) by A17, A19, XREAL_1:9;
then ( 1 <= i1 & i1 <= card A ) by A13, NAT_1:14;
then i1 in dom (SgmX ((RelIncl n),A)) by A18, FINSEQ_3:25;
then ( (C1 . (i1 + 1)) ^2 = f . ((SgmX ((RelIncl n),A)) . i1) & f . ((SgmX ((RelIncl n),A)) . i1) = (C2 . (i1 + 1)) ^2 & Re (C2 . (i1 + 1)) >= 0 & Im (C2 . (i1 + 1)) >= 0 & Re (C1 . (i1 + 1)) >= 0 & Im (C1 . (i1 + 1)) >= 0 ) by A14, A16;
hence C1 . i = C2 . i by Th2; :: thesis: verum

end;

end;

end;

hence C1 = C2 by A13, A15, FINSEQ_1:14; :: thesis: verum