let A be symmetrical Subset of COMPLEX ; :: thesis: for F being PartFunc of REAL ,REAL holds
( F is_even_on A iff ( A c= dom F & ( for x being Real st x in A holds
(F . x) - (F . (- x)) = 0 ) ) )
let F be PartFunc of REAL ,REAL ; :: thesis: ( F is_even_on A iff ( A c= dom F & ( for x being Real st x in A holds
(F . x) - (F . (- x)) = 0 ) ) )
B1: ( F is_even_on A implies ( A c= dom F & ( for x being Real st x in A holds
(F . x) - (F . (- x)) = 0 ) ) )

proof

assume A1: F is_even_on A ; :: thesis: ( A c= dom F & ( for x being Real st x in A holds
(F . x) - (F . (- x)) = 0 ) )
then A2: ( A c= dom F & F | A is even ) by Def5;
for x being Real st x in A holds
(F . x) - (F . (- x)) = 0

proof

let x be Real; :: thesis: ( x in A implies (F . x) - (F . (- x)) = 0 )
assume A5: x in A ; :: thesis: (F . x) - (F . (- x)) = 0
then A4: ( x in A & - x in A ) by Def1;
then A6: ( x in dom (F | A) & - x in dom (F | A) ) by RELAT_1:91, A2;
(F . x) - (F . (- x)) = (F /. x) - (F . (- x)) by A2, A5, PARTFUN1:def 8
.= (F /. x) - (F /. (- x)) by A2, A4, PARTFUN1:def 8
.= ((F | A) /. x) - (F /. (- x)) by PARTFUN2:35, A2, A5
.= ((F | A) /. x) - ((F | A) /. (- x)) by PARTFUN2:35, A2, A4
.= ((F | A) . x) - ((F | A) /. (- x)) by PARTFUN1:def 8, A6
.= ((F | A) . x) - ((F | A) . (- x)) by PARTFUN1:def 8, A6
.= ((F | A) . x) - ((F | A) . x) by A2, A6, Def3
.= 0 ;
hence (F . x) - (F . (- x)) = 0 ; :: thesis: verum

end;

hence ( A c= dom F & ( for x being Real st x in A holds
(F . x) - (F . (- x)) = 0 ) ) by A1, Def5; :: thesis: verum

end;

( A c= dom F & ( for x being Real st x in A holds
(F . x) - (F . (- x)) = 0 ) implies F is_even_on A )

proof

assume A7: ( A c= dom F & ( for x being Real st x in A holds
(F . x) - (F . (- x)) = 0 ) ) ; :: 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)) = 0 by A7;
hence F . (- x) = F . x ; :: thesis: verum

end;

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

end;

hence ( F is_even_on A iff ( A c= dom F & ( for x being Real st x in A holds
(F . x) - (F . (- x)) = 0 ) ) ) by B1; :: thesis: verum