let A be symmetrical Subset of COMPLEX; :: thesis: for F being PartFunc of REAL,REAL st F is_even_on A holds

for x being Real st x in A holds

F . x = F . |.x.|

let F be PartFunc of REAL,REAL; :: thesis: ( F is_even_on A implies for x being Real st x in A holds

F . x = F . |.x.| )

assume A1: F is_even_on A ; :: thesis: for x being Real st x in A holds

F . x = F . |.x.|

then A2: A c= dom F ;

A3: F | A is even by A1;

let x be Real; :: thesis: ( x in A implies F . x = F . |.x.| )

assume A4: x in A ; :: thesis: F . x = F . |.x.|

A5: x in dom (F | A) by A2, A4, RELAT_1:62;

A6: - x in A by A4, Def1;

then A7: - x in dom (F | A) by A2, RELAT_1:62;

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

for x being Real st x in A holds

F . x = F . |.x.|

let F be PartFunc of REAL,REAL; :: thesis: ( F is_even_on A implies for x being Real st x in A holds

F . x = F . |.x.| )

assume A1: F is_even_on A ; :: thesis: for x being Real st x in A holds

F . x = F . |.x.|

then A2: A c= dom F ;

A3: F | A is even by A1;

let x be Real; :: thesis: ( x in A implies F . x = F . |.x.| )

assume A4: x in A ; :: thesis: F . x = F . |.x.|

A5: x in dom (F | A) by A2, A4, RELAT_1:62;

A6: - x in A by A4, Def1;

then A7: - x in dom (F | A) by A2, RELAT_1:62;

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

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, PARTFUN1:def 6

.= (F | A) /. (- x) by A2, A6, PARTFUN2:17

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

.= (F | A) . x by A3, A5, A7, Def3

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

.= F /. x by A2, A4, PARTFUN2:17

.= F . x by A2, A4, PARTFUN1:def 6 ;

hence F . x = F . |.x.| ; :: thesis: verum

end;.= F /. (- x) by A2, A6, PARTFUN1:def 6

.= (F | A) /. (- x) by A2, A6, PARTFUN2:17

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

.= (F | A) . x by A3, A5, A7, Def3

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

.= F /. x by A2, A4, PARTFUN2:17

.= F . x by A2, A4, PARTFUN1:def 6 ;

hence F . x = F . |.x.| ; :: thesis: verum