let X be BCI-algebra; :: thesis: for x being Element of X st x is finite-period & x ` is finite-period holds
ord x = ord (x ` )
let x be Element of X; :: thesis: ( x is finite-period & x ` is finite-period implies ord x = ord (x ` ) )
assume that
A1: x is finite-period and
A2: x ` is finite-period ; :: thesis: ord x = ord (x ` )
set m = ord (x ` );
(x ` ) |^ (ord (x ` )) in BCK-part X by A2, Def5;
then ex zz being Element of X st
( zz = (x ` ) |^ (ord (x ` )) & 0. X <= zz ) ;
then ((x ` ) |^ (ord (x ` ))) ` = 0. X by BCIALG_1:def 11;
then ((x ` ) ` ) |^ (ord (x ` )) = 0. X by Th18;
then (((x ` ) ` ) |^ (ord (x ` ))) ` = 0. X by BCIALG_1:def 5;
then (x |^ (ord (x ` ))) ` = 0. X by Th21;
then 0. X <= x |^ (ord (x ` )) by BCIALG_1:def 11;
then A3: x |^ (ord (x ` )) in BCK-part X ;
set n = ord x;
ord (x ` ) <> 0 by A2, Def5;
then A4: ord x <= ord (x ` ) by A1, A3, Def5;
x |^ (ord x) in BCK-part X by A1, Def5;
then ex zz being Element of X st
( zz = x |^ (ord x) & 0. X <= zz ) ;
then (x |^ (ord x)) ` = 0. X by BCIALG_1:def 11;
then (x ` ) |^ (ord x) = 0. X by Th18;
then ((x ` ) |^ (ord x)) ` = 0. X by BCIALG_1:def 5;
then 0. X <= (x ` ) |^ (ord x) by BCIALG_1:def 11;
then A5: (x ` ) |^ (ord x) in BCK-part X ;
ord x <> 0 by A1, Def5;
then ord (x ` ) <= ord x by A2, A5, Def5;
hence ord x = ord (x ` ) by A4, XXREAL_0:1; :: thesis: verum