let A be symmetrical Subset of REAL ; :: thesis: absreal is_even_on A
A1: dom absreal = REAL by FUNCT_2:def 1;
A2: dom (absreal | A) = A by RELAT_1:91, A1;
for x being Real st x in dom (absreal | A) & - x in dom (absreal | A) holds
(absreal | A) . (- x) = (absreal | A) . x

proof

let x be Real; :: thesis: ( x in dom (absreal | A) & - x in dom (absreal | A) implies (absreal | A) . (- x) = (absreal | A) . x )
assume A3: ( x in dom (absreal | A) & - x in dom (absreal | A) ) ; :: thesis: (absreal | A) . (- x) = (absreal | A) . x
(absreal | A) . (- x) = (absreal | A) /. (- x) by PARTFUN1:def 8, A3
.= absreal /. (- x) by PARTFUN2:35, A2, A3, A1
.= absreal /. x by Th52
.= (absreal | A) /. x by PARTFUN2:35, A2, A3, A1
.= (absreal | A) . x by PARTFUN1:def 8, A3 ;
hence (absreal | A) . (- x) = (absreal | A) . x ; :: thesis: verum

end;

then ( absreal | A is with_symmetrical_domain & absreal | A is quasi_even ) by Def3, A2, Def2;
hence absreal is_even_on A by A1, Def5; :: thesis: verum