let X be BCI-algebra; :: thesis: for x being Element of X st x is finite-period holds
(x `) ` is finite-period
let x be Element of X; :: thesis: ( x is finite-period implies (x `) ` is finite-period )
reconsider b = (x `) ` as Element of AtomSet X by BCIALG_1:34;
assume x is finite-period ; :: thesis: (x `) ` is finite-period
then consider p being Element of NAT such that
A1: p <> 0 and
A2: x |^ p in BCK-part X ;
ex y being Element of X st
( y = x |^ p & 0. X <= y ) by A2;
then (x |^ p) ` = 0. X ;
then (b |^ p) ` = 0. X by Th21;
then 0. X <= b |^ p ;
then b |^ p in BCK-part X ;
hence (x `) ` is finite-period by A1; :: thesis: verum