let a, b be Nat; :: thesis: ( d |^ a divides n & not d |^ (a + 1) divides n & d |^ b divides n & not d |^ (b + 1) divides n implies a = b )
assume that
A10: d |^ a divides n and
A11: not d |^ (a + 1) divides n and
A12: d |^ b divides n and
A13: not d |^ (b + 1) divides n and
A14: a <> b ; :: thesis: contradiction
reconsider a = a, b = b as Element of NAT by ORDINAL1:def 13;
reconsider d1 = d as Element of NAT by ORDINAL1:def 13;

per cases ( a < b or b < a ) by A14, XXREAL_0:1;

suppose A15: a < b ; :: thesis: contradiction

then consider x being Nat such that
A16: a + x = b by NAT_1:10;
reconsider x = x as Element of NAT by ORDINAL1:def 13;

now

assume 0 + 1 > x ; :: thesis: contradiction
then x <= 0 by NAT_1:13;
then x = 0 ;
hence contradiction by A15, A16; :: thesis: verum

end;

then a + 1 <= a + x by XREAL_1:8;
then d1 |^ (a + 1) divides d1 |^ (a + x) by RADIX_1:7;
hence contradiction by A11, A12, A16, NAT_D:4; :: thesis: verum

end;

suppose A17: b < a ; :: thesis: contradiction

then consider x being Nat such that
A18: b + x = a by NAT_1:10;
reconsider x = x as Element of NAT by ORDINAL1:def 13;

now

assume 0 + 1 > x ; :: thesis: contradiction
then x <= 0 by NAT_1:13;
then x = 0 ;
hence contradiction by A17, A18; :: thesis: verum

end;

then b + 1 <= b + x by XREAL_1:8;
then d1 |^ (b + 1) divides d1 |^ (b + x) by RADIX_1:7;
hence contradiction by A10, A13, A18, NAT_D:4; :: thesis: verum

end;

end;