A1:
for x being object st x in dom f holds

ex y being object st S_{1}[x,y]

A2: dom F = dom f and

A3: for x being object st x in dom f holds

S_{1}[x,F . x]
from CLASSES1:sch 1(A1);

take F ; :: thesis: ( dom F = dom f & ( for x being complex-valued Function st x in dom F holds

F . x = f . (- x) ) )

thus dom F = dom f by A2; :: thesis: for x being complex-valued Function st x in dom F holds

F . x = f . (- x)

let x be complex-valued Function; :: thesis: ( x in dom F implies F . x = f . (- x) )

assume x in dom F ; :: thesis: F . x = f . (- x)

then S_{1}[x,F . x]
by A2, A3;

hence F . x = f . (- x) ; :: thesis: verum

ex y being object st S

proof

consider F being Function such that
let x be object ; :: thesis: ( x in dom f implies ex y being object st S_{1}[x,y] )

assume x in dom f ; :: thesis: ex y being object st S_{1}[x,y]

then reconsider a = x as complex-valued Function ;

take f . (- a) ; :: thesis: S_{1}[x,f . (- a)]

take a ; :: thesis: ( x = a & f . (- a) = f . (- a) )

thus ( x = a & f . (- a) = f . (- a) ) ; :: thesis: verum

end;assume x in dom f ; :: thesis: ex y being object st S

then reconsider a = x as complex-valued Function ;

take f . (- a) ; :: thesis: S

take a ; :: thesis: ( x = a & f . (- a) = f . (- a) )

thus ( x = a & f . (- a) = f . (- a) ) ; :: thesis: verum

A2: dom F = dom f and

A3: for x being object st x in dom f holds

S

take F ; :: thesis: ( dom F = dom f & ( for x being complex-valued Function st x in dom F holds

F . x = f . (- x) ) )

thus dom F = dom f by A2; :: thesis: for x being complex-valued Function st x in dom F holds

F . x = f . (- x)

let x be complex-valued Function; :: thesis: ( x in dom F implies F . x = f . (- x) )

assume x in dom F ; :: thesis: F . x = f . (- x)

then S

hence F . x = f . (- x) ; :: thesis: verum