let F be PartFunc of REAL ,REAL ; :: thesis: ( F is odd implies F ^2 is even )
assume A1: F is odd ; :: thesis: F ^2 is even
A2: dom F = dom (F ^2 ) by VALUED_1:11;
for x being Real st x in dom (F ^2 ) & - x in dom (F ^2 ) holds
(F ^2 ) . (- x) = (F ^2 ) . x

proof

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 A1, Def6, A2, A3
.= (F . x) ^2
.= (F ^2 ) . x by VALUED_1:11 ;
hence (F ^2 ) . (- x) = (F ^2 ) . x ; :: thesis: verum

end;

then ( F ^2 is with_symmetrical_domain & F ^2 is quasi_even ) by Def3, A1, A2, Def2;
hence F ^2 is even ; :: thesis: verum