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

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

suppose A1: 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 A1, NAT_D:6; :: thesis: not d |^ (0 + 1) divides n
not 0 divides n1 by B2, INT_2:3;
hence not d |^ (0 + 1) divides n by A1, NEWTON:11; :: thesis: verum

end;

suppose A2: 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;
A3: 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 A4: d |^ k <= n by B2, NAT_D:7;
k <= d |^ k by B1, A2, Th2, NAT_1:25;
hence k <= n1 by A4, XXREAL_0:2; :: thesis: verum

end;

A5: 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
A6: ( S₁[k] & ( for n being Nat st S₁[n] holds
n <= k ) ) from NAT_1:sch 6(A3, A5);
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 A6; :: thesis: verum

end;

end;