reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

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

suppose A3: d = 0 ; :: thesis: ex b₁ being Nat st
( d |^ b₁ divides n & not d |^ (b₁ + 1) divides n )

take 0 ; :: thesis: ( d |^ 0 divides n & not d |^ (0 + 1) divides n )
0 |^ 0 = 1 by NEWTON:4;
hence d |^ 0 divides n by A3, NAT_D:6; :: thesis: not d |^ (0 + 1) divides n
not 0 divides n1 by A2;
hence not d |^ (0 + 1) divides n by A3; :: thesis: verum

end;

suppose A4: d <> 0 ; :: thesis: ex b₁ being Nat st
( d |^ b₁ divides n & not d |^ (b₁ + 1) divides n )

defpred S₁[ Nat] means d |^ $1 divides n;
A5: for k being Nat st S₁[k] holds
k <= n1

proof

let k be Nat; :: thesis: ( S₁[k] implies k <= n1 )
assume S₁[k] ; :: thesis: k <= n1
then A6: d |^ k <= n by A2, NAT_D:7;
k <= d |^ k by A1, A4, Th2, NAT_1:25;
hence k <= n1 by A6, XXREAL_0:2; :: thesis: verum

end;

A7: ex k being Nat st S₁[k]

proof

take 0 ; :: thesis: S₁[ 0 ]
d |^ 0 = 1 by NEWTON:4;
hence S₁[ 0 ] by NAT_D:6; :: thesis: verum

end;

consider k being Nat such that
A8: ( S₁[k] & ( for n being Nat st S₁[n] holds
n <= k ) ) from NAT_1:sch 6(A5, A7);
take k ; :: thesis: ( d |^ k divides n & not d |^ (k + 1) divides n )
k + 0 < k + 1 by XREAL_1:6;
hence ( d |^ k divides n & not d |^ (k + 1) divides n ) by A8; :: thesis: verum

end;

end;