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 . (abs 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 . (abs x) )
assume F is_even_on A ; :: thesis: for x being Real st x in A holds
F . x = F . (abs x)
then A1: ( A c= dom F & F | A is even ) by Def5;
let x be Real; :: thesis: ( x in A implies F . x = F . (abs x) )
assume A2: x in A ; :: thesis: F . x = F . (abs x)
A4: ( x in A & - x in A ) by Def1, A2;
then A5: ( x in dom (F | A) & - x in dom (F | A) ) by RELAT_1:91, A1;

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

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

then F . (abs x) = F . (- x) by ABSVALUE:def 1
.= F /. (- x) by A1, A4, PARTFUN1:def 8
.= (F | A) /. (- x) by PARTFUN2:35, A1, A4
.= (F | A) . (- x) by PARTFUN1:def 8, A5
.= (F | A) . x by A1, Def3, A5
.= (F | A) /. x by PARTFUN1:def 8, A5
.= F /. x by PARTFUN2:35, A1, A2
.= F . x by A1, A2, PARTFUN1:def 8 ;
hence F . x = F . (abs x) ; :: thesis: verum

end;

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

hence F . x = F . (abs x) by ABSVALUE:def 1; :: thesis: verum

end;

suppose x = 0 ; :: thesis: F . x = F . (abs x)

hence F . x = F . (abs x) by ABSVALUE:def 1; :: thesis: verum

end;

end;