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.| ) 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.| ) implies F is_even_on A )

assume that

A1: A c= dom F and

A2: for x being Real st x in A holds

F . x = F . |.x.| ; :: thesis: F is_even_on A

A3: dom (F | A) = A by A1, RELAT_1:62;

A4: for x being Real st x in A holds

- x in A by Def1;

A5: for x being Real st x in A holds

F . (- x) = F . x

(F | A) . (- x) = (F | A) . x

hence F is_even_on A by A1; :: thesis: verum

F . x = F . |.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 . |.x.| ) implies F is_even_on A )

assume that

A1: A c= dom F and

A2: for x being Real st x in A holds

F . x = F . |.x.| ; :: thesis: F is_even_on A

A3: dom (F | A) = A by A1, RELAT_1:62;

A4: for x being Real st x in A holds

- x in A by Def1;

A5: for x being Real st x in A holds

F . (- x) = F . x

proof

for x being Real st x in dom (F | A) & - x in dom (F | A) holds
let x be Real; :: thesis: ( x in A implies F . (- x) = F . x )

assume A6: x in A ; :: thesis: F . (- x) = F . x

end;assume A6: x in A ; :: thesis: F . (- x) = F . x

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

end;

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

then F . (- x) =
F . |.x.|
by ABSVALUE:def 1

.= F . x by A2, A6 ;

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

end;.= F . x by A2, A6 ;

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

(F | A) . (- x) = (F | A) . x

proof

then
( F | A is with_symmetrical_domain & F | A is quasi_even )
by A3;
let x be Real; :: thesis: ( x in dom (F | A) & - x in dom (F | A) implies (F | A) . (- x) = (F | A) . x )

assume that

A7: x in dom (F | A) and

A8: - x in dom (F | A) ; :: thesis: (F | A) . (- x) = (F | A) . x

reconsider x = x as Element of REAL by XREAL_0:def 1;

(F | A) . (- x) = (F | A) /. (- x) by A8, PARTFUN1:def 6

.= F /. (- x) by A1, A3, A8, PARTFUN2:17

.= F . (- x) by A1, A8, PARTFUN1:def 6

.= F . x by A5, A7

.= F /. x by A1, A7, PARTFUN1:def 6

.= (F | A) /. x by A1, A3, A7, PARTFUN2:17

.= (F | A) . x by A7, PARTFUN1:def 6 ;

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

end;assume that

A7: x in dom (F | A) and

A8: - x in dom (F | A) ; :: thesis: (F | A) . (- x) = (F | A) . x

reconsider x = x as Element of REAL by XREAL_0:def 1;

(F | A) . (- x) = (F | A) /. (- x) by A8, PARTFUN1:def 6

.= F /. (- x) by A1, A3, A8, PARTFUN2:17

.= F . (- x) by A1, A8, PARTFUN1:def 6

.= F . x by A5, A7

.= F /. x by A1, A7, PARTFUN1:def 6

.= (F | A) /. x by A1, A3, A7, PARTFUN2:17

.= (F | A) . x by A7, PARTFUN1:def 6 ;

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

hence F is_even_on A by A1; :: thesis: verum