let n1, n2 be Element of NAT ; :: thesis: ( x |^ n1 in BCK-part X & n1 <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds
n1 <= m ) & x |^ n2 in BCK-part X & n2 <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds
n2 <= m ) implies n1 = n2 )
assume ( x |^ n1 in BCK-part X & n1 <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds
n1 <= m ) & x |^ n2 in BCK-part X & n2 <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds
n2 <= m ) ) ; :: thesis: n1 = n2
then ( n1 <= n2 & n2 <= n1 ) ;
hence n1 = n2 by XXREAL_0:1; :: thesis: verum