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 A3: ( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) ) ; :: thesis: F is_even_on A
B1: 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 A3;
hence F . (- x) = F . x by XCMPLX_1:58; :: thesis: verum

end;

A8: dom (F | A) = A by RELAT_1:91, A3;
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 A9: ( x in dom (F | A) & - x in dom (F | A) ) ; :: thesis: (F | A) . (- x) = (F | A) . x
(F | A) . (- x) = (F | A) /. (- x) by PARTFUN1:def 8, A9
.= F /. (- x) by PARTFUN2:35, A9, A8, A3
.= F . (- x) by PARTFUN1:def 8, A9, A8, A3
.= F . x by A9, A8, B1
.= F /. x by PARTFUN1:def 8, A9, A8, A3
.= (F | A) /. x by PARTFUN2:35, A9, A8, A3
.= (F | A) . x by PARTFUN1:def 8, A9 ;
hence (F | A) . (- x) = (F | A) . x ; :: thesis: verum

end;

then ( F | A is with_symmetrical_domain & F | A is quasi_even ) by Def3, A8, Def2;
hence F is_even_on A by A3, Def5; :: thesis: verum