let F be PartFunc of REAL,REAL; :: thesis: ( F is even implies |.F.| is even )

A1: dom F = dom |.F.| by VALUED_1:def 11;

assume A2: F is even ; :: thesis: |.F.| is even

for x being Real st x in dom |.F.| & - x in dom |.F.| holds

|.F.| . (- x) = |.F.| . x

hence |.F.| is even ; :: thesis: verum

A1: dom F = dom |.F.| by VALUED_1:def 11;

assume A2: F is even ; :: thesis: |.F.| is even

for x being Real st x in dom |.F.| & - x in dom |.F.| holds

|.F.| . (- x) = |.F.| . x

proof

then
( |.F.| is with_symmetrical_domain & |.F.| is quasi_even )
by A2, A1;
let x be Real; :: thesis: ( x in dom |.F.| & - x in dom |.F.| implies |.F.| . (- x) = |.F.| . x )

assume that

A3: x in dom |.F.| and

A4: - x in dom |.F.| ; :: thesis: |.F.| . (- x) = |.F.| . x

|.F.| . (- x) = |.(F . (- x)).| by A4, VALUED_1:def 11

.= |.(F . x).| by A2, A1, A3, A4, Def3

.= |.F.| . x by A3, VALUED_1:def 11 ;

hence |.F.| . (- x) = |.F.| . x ; :: thesis: verum

end;assume that

A3: x in dom |.F.| and

A4: - x in dom |.F.| ; :: thesis: |.F.| . (- x) = |.F.| . x

|.F.| . (- x) = |.(F . (- x)).| by A4, VALUED_1:def 11

.= |.(F . x).| by A2, A1, A3, A4, Def3

.= |.F.| . x by A3, VALUED_1:def 11 ;

hence |.F.| . (- x) = |.F.| . x ; :: thesis: verum

hence |.F.| is even ; :: thesis: verum