let r be Real; :: thesis: for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL ,REAL st F is_even_on A holds
F - r is_even_on A
let A be symmetrical Subset of COMPLEX ; :: thesis: for F being PartFunc of REAL ,REAL st F is_even_on A holds
F - r is_even_on A
let F be PartFunc of REAL ,REAL ; :: thesis: ( F is_even_on A implies F - r is_even_on A )
assume A1: F is_even_on A ; :: thesis: F - r is_even_on A
then A2: A c= dom F by Def5;
then A3: A c= dom (F - r) by VALUED_1:3;
then A4: dom ((F - r) | A) = A by RELAT_1:91;
A5: F | A is even by A1, Def5;
for x being Real st x in dom ((F - r) | A) & - x in dom ((F - r) | A) holds
((F - r) | A) . (- x) = ((F - r) | A) . x

proof

let x be Real; :: thesis: ( x in dom ((F - r) | A) & - x in dom ((F - r) | A) implies ((F - r) | A) . (- x) = ((F - r) | A) . x )
assume that
A6: x in dom ((F - r) | A) and
A7: - x in dom ((F - r) | A) ; :: thesis: ((F - r) | A) . (- x) = ((F - r) | A) . x
A8: x in dom (F | A) by A2, A4, A6, RELAT_1:91;
A9: - x in dom (F | A) by A2, A4, A7, RELAT_1:91;
((F - r) | A) . (- x) = ((F - r) | A) /. (- x) by A7, PARTFUN1:def 8
.= (F - r) /. (- x) by A3, A4, A7, PARTFUN2:35
.= (F - r) . (- x) by A3, A4, A7, PARTFUN1:def 8
.= (F . (- x)) - r by A2, A4, A7, VALUED_1:3
.= (F /. (- x)) - r by A2, A4, A7, PARTFUN1:def 8
.= ((F | A) /. (- x)) - r by A2, A4, A7, PARTFUN2:35
.= ((F | A) . (- x)) - r by A9, PARTFUN1:def 8
.= ((F | A) . x) - r by A5, A8, A9, Def3
.= ((F | A) /. x) - r by A8, PARTFUN1:def 8
.= (F /. x) - r by A2, A4, A6, PARTFUN2:35
.= (F . x) - r by A2, A4, A6, PARTFUN1:def 8
.= (F - r) . x by A2, A4, A6, VALUED_1:3
.= (F - r) /. x by A3, A4, A6, PARTFUN1:def 8
.= ((F - r) | A) /. x by A3, A4, A6, PARTFUN2:35
.= ((F - r) | A) . x by A6, PARTFUN1:def 8 ;
hence ((F - r) | A) . (- x) = ((F - r) | A) . x ; :: thesis: verum

end;

then ( (F - r) | A is with_symmetrical_domain & (F - r) | A is quasi_even ) by A4, Def2, Def3;
hence F - r is_even_on A by A3, Def5; :: thesis: verum