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 ;
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 `)) ;
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 ;
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) ;
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