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.|) )
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 Th6; :: thesis: verum