let F be PartFunc of REAL,REAL; :: thesis: ( F is even implies F ^2 is even )

A1: dom F = dom (F ^2) by VALUED_1:11;

assume A2: F is even ; :: thesis: F ^2 is even

for x being Real st x in dom (F ^2) & - x in dom (F ^2) holds

(F ^2) . (- x) = (F ^2) . x

hence F ^2 is even ; :: thesis: verum

A1: dom F = dom (F ^2) by VALUED_1:11;

assume A2: F is even ; :: thesis: F ^2 is even

for x being Real st x in dom (F ^2) & - x in dom (F ^2) holds

(F ^2) . (- x) = (F ^2) . x

proof

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

assume A3: ( x in dom (F ^2) & - x in dom (F ^2) ) ; :: thesis: (F ^2) . (- x) = (F ^2) . x

(F ^2) . (- x) = (F . (- x)) ^2 by VALUED_1:11

.= (F . x) ^2 by A2, A1, A3, Def3

.= (F ^2) . x by VALUED_1:11 ;

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

end;assume A3: ( x in dom (F ^2) & - x in dom (F ^2) ) ; :: thesis: (F ^2) . (- x) = (F ^2) . x

(F ^2) . (- x) = (F . (- x)) ^2 by VALUED_1:11

.= (F . x) ^2 by A2, A1, A3, Def3

.= (F ^2) . x by VALUED_1:11 ;

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

hence F ^2 is even ; :: thesis: verum