let n, k be Nat; :: thesis: for a being non trivial Nat st (Py (a,k)) ^2 divides Py (a,n) holds
Py (a,k) divides n
let a be non trivial Nat; :: thesis: ( (Py (a,k)) ^2 divides Py (a,n) implies Py (a,k) divides n )
assume A1: (Py (a,k)) ^2 divides Py (a,n) ; :: thesis: Py (a,k) divides n

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

suppose k = 0 ; :: thesis: Py (a,k) divides n

then Py (a,k) = 0 by Th6;
then ex i being Integer st 0 * i = Py (a,n) by A1, INT_1:def 3;
then (Py (a,k)) * 0 = n ;
hence Py (a,k) divides n by INT_1:def 3; :: thesis: verum

end;

suppose A2: k > 0 ; :: thesis: Py (a,k) divides n

Py (a,k) divides (Py (a,k)) ^2 by INT_1:def 3;
then Py (a,k) divides Py (a,n) by A1, INT_2:9;
then consider w being Nat such that
A3: k * w = n by NAT_D:def 3, Th39, A2;
A4: w divides n by A3, NAT_D:def 3;
(Py (a,k)) ^2 divides (Py (a,n)) - 0 by A1;
then A5: 0 , Py (a,n) are_congruent_mod (Py (a,k)) ^2 by INT_1:14, INT_1:def 4;
Py (a,n),(w * ((Px (a,k)) |^ (w -' 1))) * (Py (a,k)) are_congruent_mod (Py (a,k)) ^2 by Th38, A3;
then A6: 0 * ((Px (a,k)) |^ (w -' 1)),(w * (Py (a,k))) * ((Px (a,k)) |^ (w -' 1)) are_congruent_mod (Py (a,k)) ^2 by A5, INT_1:15;
A8: (Py (a,k)) ^2 = (Py (a,k)) * ((Py (a,k)) |^ 1)
.= (Py (a,k)) |^ (1 + 1) by NEWTON:6 ;
Py (a,k), Px (a,k) are_coprime by Th26;
then (Py (a,k)) |^ 2, Px (a,k) are_coprime by WSIERP_1:10;
then 0 ,w * (Py (a,k)) are_congruent_mod (Py (a,k)) ^2 by A6, A8, INT_4:9, WSIERP_1:10;
then (Py (a,k)) ^2 divides (w * (Py (a,k))) - 0 by INT_1:def 4, INT_1:14;
then ( Py (a,k) divides w or Py (a,k) = 0 ) by PYTHTRIP:7;
hence Py (a,k) divides n by A4, A2, INT_2:9; :: thesis: verum

end;

end;