let x be Integer; :: thesis: for a being non trivial Nat st x <= 0 holds
(sgn x) * (Py (a,|.x.|)) = - (Py (a,|.x.|))
let a be non trivial Nat; :: thesis: ( x <= 0 implies (sgn x) * (Py (a,|.x.|)) = - (Py (a,|.x.|)) )
A1: Py (a,|.0.|) = 0 by Th6;
assume x <= 0 ; :: thesis: (sgn x) * (Py (a,|.x.|)) = - (Py (a,|.x.|))
then ( x = 0 or x < 0 ) ;
then ( sgn x = - 1 or ( sgn x = 0 & x = 0 ) ) by ABSVALUE:def 2;
hence (sgn x) * (Py (a,|.x.|)) = - (Py (a,|.x.|)) by A1; :: thesis: verum