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 )
assume A1: x is finite-period ; :: thesis: (x ` ) ` is finite-period
reconsider b = (x ` ) ` as Element of AtomSet X by BCIALG_1:34;
consider p being Element of NAT such that
C71: ( p <> 0 & x |^ p in BCK-part X ) by A1, Defx1;
consider y being Element of X such that
C72: ( y = x |^ p & 0. X <= y ) by C71;
(x |^ p) ` = 0. X by C72, BCIALG_1:def 11;
then (b |^ p) ` = 0. X by Th19;
then 0. X <= b |^ p by BCIALG_1:def 11;
then b |^ p in BCK-part X ;
hence (x ` ) ` is finite-period by Defx1, C71; :: thesis: verum