let n be Nat; :: thesis: for a being non trivial Nat holds Py (a,(2 * n)) = (2 * (Py (a,n))) * (Px (a,n))
let a be non trivial Nat; :: thesis: Py (a,(2 * n)) = (2 * (Py (a,n))) * (Px (a,n))
A1: Py (a,0) = 0 by HILB10_1:3;

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: Py (a,(2 * n)) = (2 * (Py (a,n))) * (Px (a,n))

hence Py (a,(2 * n)) = (2 * (Py (a,n))) * (Px (a,n)) by A1; :: thesis: verum

end;

suppose n > 0 ; :: thesis: Py (a,(2 * n)) = (2 * (Py (a,n))) * (Px (a,n))

then A2: ( sgn n = 1 & sgn (n + n) = 1 ) by ABSVALUE:def 2;
(sgn (n + n)) * (Py (a,|.(n + n).|)) = (((Px (a,|.n.|)) * (sgn n)) * (Py (a,|.n.|))) + (((sgn n) * (Py (a,|.n.|))) * (Px (a,|.n.|))) by HILB10_1:22;
hence Py (a,(2 * n)) = (2 * (Py (a,n))) * (Px (a,n)) by A2; :: thesis: verum

end;

end;