let A be symmetrical Subset of COMPLEX; :: thesis: for F being PartFunc of REAL,REAL st A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) holds
F is_even_on A
let F be PartFunc of REAL,REAL; :: thesis: ( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) implies F is_even_on A )
assume that
A1: A c= dom F and
A2: for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ; :: thesis: F is_even_on A
A3: dom (F | A) = A by A1, RELAT_1:62;
A4: for x being Real st x in A holds
F . (- x) = F . x

proof

let x be Real; :: thesis: ( x in A implies F . (- x) = F . x )
assume x in A ; :: thesis: F . (- x) = F . x
then (F . x) / (F . (- x)) = 1 by A2;
hence F . (- x) = F . x by XCMPLX_1:58; :: thesis: verum

end;

for x being Real st x in dom (F | A) & - x in dom (F | A) holds
(F | A) . (- x) = (F | A) . x

proof

let x be Real; :: thesis: ( x in dom (F | A) & - x in dom (F | A) implies (F | A) . (- x) = (F | A) . x )
assume that
A5: x in dom (F | A) and
A6: - x in dom (F | A) ; :: thesis: (F | A) . (- x) = (F | A) . x
reconsider x = x as Element of REAL by XREAL_0:def 1;
(F | A) . (- x) = (F | A) /. (- x) by A6, PARTFUN1:def 6
.= F /. (- x) by A1, A3, A6, PARTFUN2:17
.= F . (- x) by A1, A6, PARTFUN1:def 6
.= F . x by A4, A5
.= F /. x by A1, A5, PARTFUN1:def 6
.= (F | A) /. x by A1, A3, A5, PARTFUN2:17
.= (F | A) . x by A5, PARTFUN1:def 6 ;
hence (F | A) . (- x) = (F | A) . x ; :: thesis: verum

end;

then ( F | A is with_symmetrical_domain & F | A is quasi_even ) by A3;
hence F is_even_on A by A1; :: thesis: verum