let n, k be Nat; :: thesis: for a being non trivial Nat holds Py (a,n) divides Py (a,(n * k))
let a be non trivial Nat; :: thesis: Py (a,n) divides Py (a,(n * k))
defpred S₁[ Nat] means Py (a,n) divides Py (a,(n * $1));
(Py (a,n)) * 0 = Py (a,(n * 0)) by Th6;
then A1: S₁[ 0 ] by INT_1:def 3;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
A4: ( Py (a,((n * k) + n)) = (sgn ((n * k) + n)) * (Py (a,|.((n * k) + n).|)) & (sgn n) * (Py (a,|.n.|)) = Py (a,n) & (sgn (n * k)) * (Py (a,|.(n * k).|)) = Py (a,(n * k)) ) by Th23;
then A5: Py (a,|.((n * k) + n).|) = (((Px (a,|.(n * k).|)) * (sgn n)) * (Py (a,|.n.|))) + (((sgn (n * k)) * (Py (a,|.(n * k).|))) * (Px (a,|.n.|))) by Th25
.= ((Px (a,(n * k))) * (Py (a,n))) + ((Py (a,(n * k))) * (Px (a,n))) by A4 ;
A6: Py (a,n) divides (Py (a,(n * k))) * (Px (a,n)) by A3, INT_2:2;
Py (a,n) divides (Px (a,(n * k))) * (Py (a,n)) by NAT_D:9;
hence S₁[k + 1] by A5, A6, NAT_D:8; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence Py (a,n) divides Py (a,(n * k)) ; :: thesis: verum