let A be symmetrical Subset of COMPLEX ; :: thesis: for F being PartFunc of REAL ,REAL st F is_even_on A holds
|.F.| is_even_on A
let F be PartFunc of REAL ,REAL ; :: thesis: ( F is_even_on A implies |.F.| is_even_on A )
assume F is_even_on A ; :: thesis: |.F.| is_even_on A
then A1: ( A c= dom F & F | A is even ) by Def5;
A2: A c= dom |.F.| by A1, VALUED_1:def 11;
A3: dom (|.F.| | A) = A by RELAT_1:91, A2;
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 A5: ( x in dom (|.F.| | A) & - x in dom (|.F.| | A) ) ; :: thesis: (|.F.| | A) . (- x) = (|.F.| | A) . x
then A6: ( x in dom (F | A) & - x in dom (F | A) ) by RELAT_1:91, A1, A3;
(|.F.| | A) . (- x) = (|.F.| | A) /. (- x) by PARTFUN1:def 8, A5
.= |.F.| /. (- x) by PARTFUN2:35, A2, A3, A5
.= |.F.| . (- x) by PARTFUN1:def 8, A2, A3, A5
.= |.(F . (- x)).| by VALUED_1:def 11, A2, A3, A5
.= |.(F /. (- x)).| by PARTFUN1:def 8, A3, A1, A5
.= |.((F | A) /. (- x)).| by PARTFUN2:35, A1, A3, A5
.= |.((F | A) . (- x)).| by PARTFUN1:def 8, A6
.= |.((F | A) . x).| by A1, Def3, A6
.= |.((F | A) /. x).| by PARTFUN1:def 8, A6
.= |.(F /. x).| by PARTFUN2:35, A1, A3, A5
.= |.(F . x).| by PARTFUN1:def 8, A1, A3, A5
.= |.F.| . x by VALUED_1:def 11, A2, A3, A5
.= |.F.| /. x by PARTFUN1:def 8, A2, A3, A5
.= (|.F.| | A) /. x by PARTFUN2:35, A2, A3, A5
.= (|.F.| | A) . x by PARTFUN1:def 8, A5 ;
hence (|.F.| | A) . (- x) = (|.F.| | A) . x ; :: thesis: verum

end;

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