A1: for x being object st x in dom f holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in dom f implies ex y being object st S₁[x,y] )
assume x in dom f ; :: thesis: ex y being object st S₁[x,y]
then reconsider a = x as complex-valued Function ;
take f . (- a) ; :: thesis: S₁[x,f . (- a)]
take a ; :: thesis: ( x = a & f . (- a) = f . (- a) )
thus ( x = a & f . (- a) = f . (- a) ) ; :: thesis: verum

end;

consider F being Function such that
A2: dom F = dom f and
A3: for x being object st x in dom f holds
S₁[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₁[x,F . x] by A2, A3;
hence F . x = f . (- x) ; :: thesis: verum