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 A1: F is_even_on A ; :: thesis: |.F.| is_even_on A
then A2: A c= dom F ;
then A3: A c= dom |.F.| by VALUED_1:def 11;
then A4: dom (|.F.| | A) = A by RELAT_1:62;
A5: F | A is even by 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 that
A6: x in dom (|.F.| | A) and
A7: - x in dom (|.F.| | A) ; :: thesis: (|.F.| | A) . (- x) = (|.F.| | A) . x
A8: x in dom (F | A) by A2, A4, A6, RELAT_1:62;
A9: - x in dom (F | A) by A2, A4, A7, RELAT_1:62;
reconsider x = x as Element of REAL by XREAL_0:def 1;
(|.F.| | A) . (- x) = (|.F.| | A) /. (- x) by A7, PARTFUN1:def 6
.= |.F.| /. (- x) by A3, A4, A7, PARTFUN2:17
.= |.F.| . (- x) by A3, A7, PARTFUN1:def 6
.= |.(F . (- x)).| by A3, A7, VALUED_1:def 11
.= |.(F /. (- x)).| by A2, A7, PARTFUN1:def 6
.= |.((F | A) /. (- x)).| by A2, A4, A7, PARTFUN2:17
.= |.((F | A) . (- x)).| by A9, PARTFUN1:def 6
.= |.((F | A) . x).| by A5, A8, A9, Def3
.= |.((F | A) /. x).| by A8, PARTFUN1:def 6
.= |.(F /. x).| by A2, A4, A6, PARTFUN2:17
.= |.(F . x).| by A2, A6, PARTFUN1:def 6
.= |.F.| . x by A3, A6, VALUED_1:def 11
.= |.F.| /. x by A3, A6, PARTFUN1:def 6
.= (|.F.| | A) /. x by A3, A4, A6, PARTFUN2:17
.= (|.F.| | A) . x by A6, 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 A4;
hence |.F.| is_even_on A by A3; :: thesis: verum