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;

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

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;

suppose 0 < x ; :: thesis: F . x = F . |.x.|

hence F . x = F . |.x.| by ABSVALUE:def 1; :: thesis: verum

end;

suppose x = 0 ; :: thesis: F . x = F . |.x.|

hence F . x = F . |.x.| by ABSVALUE:def 1; :: thesis: verum

end;

end;