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 A1: ( x is finite-period & x ` is finite-period ) ; :: thesis: ord x = ord (x ` )
set n = ord x;
set m = ord (x ` );
x |^ (ord x) in BCK-part X by Def8a, A1;
then consider zz being Element of X such that
A3: ( zz = x |^ (ord x) & 0. X <= zz ) ;
(x |^ (ord x)) ` = 0. X by A3, BCIALG_1:def 11;
then (x ` ) |^ (ord x) = 0. X by Th17b;
then ((x ` ) |^ (ord x)) ` = 0. X by BCIALG_1:def 5;
then 0. X <= (x ` ) |^ (ord x) by BCIALG_1:def 11;
then ( (x ` ) |^ (ord x) in BCK-part X & ord x <> 0 ) by Def8a, A1;
then C1: ord (x ` ) <= ord x by Def8a, A1;
(x ` ) |^ (ord (x ` )) in BCK-part X by Def8a, A1;
then consider zz being Element of X such that
A3: ( zz = (x ` ) |^ (ord (x ` )) & 0. X <= zz ) ;
((x ` ) |^ (ord (x ` ))) ` = 0. X by A3, BCIALG_1:def 11;
then ((x ` ) ` ) |^ (ord (x ` )) = 0. X by Th17b;
then (((x ` ) ` ) |^ (ord (x ` ))) ` = 0. X by BCIALG_1:def 5;
then (x |^ (ord (x ` ))) ` = 0. X by Th19;
then 0. X <= x |^ (ord (x ` )) by BCIALG_1:def 11;
then ( x |^ (ord (x ` )) in BCK-part X & ord (x ` ) <> 0 ) by Def8a, A1;
then ord x <= ord (x ` ) by Def8a, A1;
hence ord x = ord (x ` ) by C1, XXREAL_0:1; :: thesis: verum