let x be object ; :: thesis: for f being FinSequence of F_Complex
for A being set ex i being Integer st
( ( i = 1 or i = - 1 ) & (SignGen (f, the addF of F_Complex,A)) . x = i * (f . x) )
set AF = the addF of F_Complex;
let f be FinSequence of F_Complex; :: thesis: for A being set ex i being Integer st
( ( i = 1 or i = - 1 ) & (SignGen (f, the addF of F_Complex,A)) . x = i * (f . x) )
let A be set ; :: thesis: ex i being Integer st
( ( i = 1 or i = - 1 ) & (SignGen (f, the addF of F_Complex,A)) . x = i * (f . x) )
A1: dom (SignGen (f, the addF of F_Complex,A)) = dom f by HILB10_7:def 11;

per cases ( not x in dom f or x in dom f ) ;

suppose not x in dom f ; :: thesis: ex i being Integer st
( ( i = 1 or i = - 1 ) & (SignGen (f, the addF of F_Complex,A)) . x = i * (f . x) )

then ( (SignGen (f, the addF of F_Complex,A)) . x = 0 & f . x = 0 ) by A1, FUNCT_1:def 2;
then (SignGen (f, the addF of F_Complex,A)) . x = 1 * (f . x) ;
hence ex i being Integer st
( ( i = 1 or i = - 1 ) & (SignGen (f, the addF of F_Complex,A)) . x = i * (f . x) ) ; :: thesis: verum

end;

suppose A2: x in dom f ; :: thesis: ex i being Integer st
( ( i = 1 or i = - 1 ) & (SignGen (f, the addF of F_Complex,A)) . x = i * (f . x) )

then A3: f . x = f /. x by PARTFUN1:def 6;

per cases ( x in A or not x in A ) ;

suppose x in A ; :: thesis: ex i being Integer st
( ( i = 1 or i = - 1 ) & (SignGen (f, the addF of F_Complex,A)) . x = i * (f . x) )

then (SignGen (f, the addF of F_Complex,A)) . x = (the_inverseOp_wrt the addF of F_Complex) . (f . x) by A1, A2, HILB10_7:def 11
.= (comp F_Complex) . (f . x) by FVSUM_1:15
.= - (f /. x) by A3, VECTSP_1:def 13
.= - (f . x) by A2, PARTFUN1:def 6, COMPLFLD:2
.= (- 1) * (f . x) ;
hence ex i being Integer st
( ( i = 1 or i = - 1 ) & (SignGen (f, the addF of F_Complex,A)) . x = i * (f . x) ) ; :: thesis: verum

end;

suppose not x in A ; :: thesis: ex i being Integer st
( ( i = 1 or i = - 1 ) & (SignGen (f, the addF of F_Complex,A)) . x = i * (f . x) )

then (SignGen (f, the addF of F_Complex,A)) . x = 1 * (f . x) by A1, A2, HILB10_7:def 11;
hence ex i being Integer st
( ( i = 1 or i = - 1 ) & (SignGen (f, the addF of F_Complex,A)) . x = i * (f . x) ) ; :: thesis: verum

end;

end;

end;

end;