let x be Integer; :: thesis: for a being non trivial Nat holds ((sgn x) * (sgn x)) * (Py (a,|.x.|)) = Py (a,|.x.|)
let a be non trivial Nat; :: thesis: ((sgn x) * (sgn x)) * (Py (a,|.x.|)) = Py (a,|.x.|)

per cases ( x >= 0 or x <= 0 ) ;

suppose A1: x >= 0 ; :: thesis: ((sgn x) * (sgn x)) * (Py (a,|.x.|)) = Py (a,|.x.|)

thus ((sgn x) * (sgn x)) * (Py (a,|.x.|)) = (sgn x) * ((sgn x) * (Py (a,|.x.|)))
.= (sgn x) * (Py (a,|.x.|)) by A1, Th23
.= Py (a,|.x.|) by A1, Th23 ; :: thesis: verum

end;

suppose A2: x <= 0 ; :: thesis: ((sgn x) * (sgn x)) * (Py (a,|.x.|)) = Py (a,|.x.|)

thus ((sgn x) * (sgn x)) * (Py (a,|.x.|)) = (sgn x) * ((sgn x) * (Py (a,|.x.|)))
.= (sgn x) * (- (Py (a,|.x.|))) by A2, Th24
.= - ((sgn x) * (Py (a,|.x.|)))
.= - (- (Py (a,|.x.|))) by A2, Th24
.= Py (a,|.x.|) ; :: thesis: verum

end;

end;