let X be BCI-algebra; :: thesis: for a being Element of AtomSet X
for i being Integer holds a |^ i in AtomSet X
let a be Element of AtomSet X; :: thesis: for i being Integer holds a |^ i in AtomSet X
let i be Integer; :: thesis: a |^ i in AtomSet X
defpred S₁[ Integer] means a |^ $1 in AtomSet X;
0. X in AtomSet X ;
then A3: S₁[ 0 ] by Def1;

per cases ( i >= 0 or i <= 0 ) ;

suppose A4: i >= 0 ; :: thesis: a |^ i in AtomSet X

A5: for i2 being Integer st i2 >= 0 & S₁[i2] holds
S₁[i2 + 1]

proof

let i2 be Integer; :: thesis: ( i2 >= 0 & S₁[i2] implies S₁[i2 + 1] )
assume B1: i2 >= 0 ; :: thesis: ( not S₁[i2] or S₁[i2 + 1] )
assume B3: S₁[i2] ; :: thesis: S₁[i2 + 1]
reconsider j = i2 as Element of NAT by B1, INT_1:16;
((a |^ (j + 1)) ` ) ` = ((a \ ((a |^ j) ` )) ` ) ` by Def1;
then ((a |^ (j + 1)) ` ) ` = ((a ` ) \ (((a |^ j) ` ) ` )) ` by BCIALG_1:9;
then ((a |^ (j + 1)) ` ) ` = ((a ` ) ` ) \ ((((a |^ j) ` ) ` ) ` ) by BCIALG_1:9;
then ((a |^ (j + 1)) ` ) ` = a \ ((((a |^ j) ` ) ` ) ` ) by BCIALG_1:29;
then ((a |^ (j + 1)) ` ) ` = a \ ((a |^ j) ` ) by B3, BCIALG_1:29;
then ((a |^ (j + 1)) ` ) ` = a |^ (j + 1) by Def1;
hence S₁[i2 + 1] by BCIALG_1:29; :: thesis: verum

end;

for i being Integer st i >= 0 holds
S₁[i] from INT_1:sch 2(A3, A5);
hence a |^ i in AtomSet X by A4; :: thesis: verum

end;

suppose A6: i <= 0 ; :: thesis: a |^ i in AtomSet X

A7: for i2 being Integer st i2 <= 0 & S₁[i2] holds
S₁[i2 - 1]

proof

let i2 be Integer; :: thesis: ( i2 <= 0 & S₁[i2] implies S₁[i2 - 1] )
assume B1: i2 <= 0 ; :: thesis: ( not S₁[i2] or S₁[i2 - 1] )
assume B3: S₁[i2] ; :: thesis: S₁[i2 - 1]

per cases ( i2 = 0 or i2 < 0 ) by B1;

suppose D1: i2 = 0 ; :: thesis: S₁[i2 - 1]

((a ` ) ` ) ` = a ` by BCIALG_1:8;
then a ` in AtomSet X by BCIALG_1:29;
hence S₁[i2 - 1] by D1, Th4; :: thesis: verum

end;

suppose D1: i2 < 0 ; :: thesis: S₁[i2 - 1]

set j = i2;
reconsider m = - i2 as Element of NAT by D1, INT_1:16;
a |^ (i2 - 1) = (BCI-power X) . (a ` ),(abs (i2 - 1)) by Def2, D1;
then a |^ (i2 - 1) = (BCI-power X) . (a ` ),(- (i2 - 1)) by D1, ABSVALUE:def 1;
then a |^ (i2 - 1) = (a ` ) |^ (m + 1) ;
then a |^ (i2 - 1) = (a ` ) \ (((a ` ) |^ m) ` ) by Def1;
then a |^ (i2 - 1) = (a ` ) \ ((a |^ (- (- i2))) ` ) by Th9;
then ((a |^ (i2 - 1)) ` ) ` = (((a ` ) ` ) \ (((a |^ i2) ` ) ` )) ` by BCIALG_1:9;
then ((a |^ (i2 - 1)) ` ) ` = (a \ (((a |^ i2) ` ) ` )) ` by BCIALG_1:29;
then ((a |^ (i2 - 1)) ` ) ` = (a \ (a |^ i2)) ` by B3, BCIALG_1:29;
then ((a |^ (i2 - 1)) ` ) ` = (a ` ) \ ((a |^ (- m)) ` ) by BCIALG_1:9;
then ((a |^ (i2 - 1)) ` ) ` = (a ` ) \ (((a ` ) |^ m) ` ) by Th9;
then ((a |^ (i2 - 1)) ` ) ` = (a ` ) |^ (m + 1) by Def1;
then ((a |^ (i2 - 1)) ` ) ` = (BCI-power X) . (a ` ),(- (i2 - 1)) ;
then ((a |^ (i2 - 1)) ` ) ` = (BCI-power X) . (a ` ),(abs (i2 - 1)) by D1, ABSVALUE:def 1;
then ((a |^ (i2 - 1)) ` ) ` = a |^ (i2 - 1) by Def2, D1;
hence S₁[i2 - 1] by BCIALG_1:29; :: thesis: verum

end;

end;

end;

for i being Integer st i <= 0 holds
S₁[i] from INT_1:sch 3(A3, A7);
hence a |^ i in AtomSet X by A6; :: thesis: verum

end;

end;