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 . (abs x) ) 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 . (abs x) ) implies F is_even_on A )
assume that
A1: A c= dom F and
B1: for x being Real st x in A holds
F . x = F . (abs x) ; :: thesis: F is_even_on A
B2: for x being Real st x in A holds
- x in A by Def1;
B3: 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 A2: x in A ; :: thesis: F . (- x) = F . x

per cases ( x < 0 or 0 < x or x = 0 ) ;

suppose x < 0 ; :: thesis: F . (- x) = F . x

then F . (- x) = F . (abs x) by ABSVALUE:def 1
.= F . x by B1, A2 ;
hence F . (- x) = F . x ; :: thesis: verum

end;

suppose 0 < x ; :: thesis: F . (- x) = F . x

then abs (- x) = - (- x) by ABSVALUE:def 1
.= x ;
hence F . (- x) = F . x by B1, B2, A2; :: thesis: verum

end;

suppose x = 0 ; :: thesis: F . (- x) = F . x

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

end;

end;

end;

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