let X be BCI-algebra; :: thesis: for x being Element of X st x is nilpotent holds
ord x = ord (x `)
let x be Element of X; :: thesis: ( x is nilpotent implies ord x = ord (x `) )
assume A1: x is nilpotent ; :: thesis: ord x = ord (x `)
then consider k being non zero Nat such that
A2: ((0. X),x) to_power k = 0. X ;
A3: x ` is nilpotent
proof
take k ; :: according to BCIALG_2:def 6 :: thesis: ((0. X),(x `)) to_power k = 0. X
((0. X),(x `)) to_power k = (((0. X),x) to_power k) ` by Th9
.= 0. X by A2, BCIALG_1:def 5 ;
hence ((0. X),(x `)) to_power k = 0. X ; :: thesis: verum
end;
set k = ord x;
A4: now :: thesis: for m being Nat st ((0. X),(x `)) to_power m = 0. X & m <> 0 holds
ord x <= m
let m be Nat; :: thesis: ( ((0. X),(x `)) to_power m = 0. X & m <> 0 implies ord x <= m )
assume that
A5: ((0. X),(x `)) to_power m = 0. X and
A6: m <> 0 ; :: thesis: ord x <= m
(((0. X),x) to_power m) ` = 0. X by A5, Th9;
then ((((0. X),x) to_power m) `) ` = 0. X by BCIALG_1:def 5;
then ((0. X),x) to_power m = 0. X by Th12;
hence ord x <= m by A1, A6, Def8; :: thesis: verum
end;
((0. X),(x `)) to_power (ord x) = (((0. X),x) to_power (ord x)) ` by Th9
.= (0. X) ` by A1, Def8
.= 0. X by BCIALG_1:def 5 ;
hence ord x = ord (x `) by A3, A4, Def8; :: thesis: verum