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 A1: S₁[ 0 ] by Def1;

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

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

A3: 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 i2 >= 0 ; :: thesis: ( not S₁[i2] or S₁[i2 + 1] )
then reconsider j = i2 as Element of NAT by 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 A4: ((a |^ (j + 1)) ` ) ` = a \ ((((a |^ j) ` ) ` ) ` ) by BCIALG_1:29;
assume S<sub>1</sub>[i2] ; :: thesis: S<sub>1</sub>[i2 + 1]
then ((a |^ (j + 1)) ` ) ` = a \ ((a |^ j) ` ) by A4, 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(A1, A3);
hence a |^ i in AtomSet X by A2; :: thesis: verum

end;

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

A6: 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 A7: i2 <= 0 ; :: thesis: ( not S₁[i2] or S₁[i2 - 1] )
assume A8: S₁[i2] ; :: thesis: S₁[i2 - 1]

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

suppose A9: 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 A9, Th5; :: thesis: verum

end;

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

set j = i2;
reconsider m = - i2 as Element of NAT by A10, INT_1:16;
a |^ (i2 - 1) = (BCI-power X) . (a ` ),(abs (i2 - 1)) by A10, Def2;
then a |^ (i2 - 1) = (BCI-power X) . (a ` ),(- (i2 - 1)) by A10, 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 Th10;
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 A8, BCIALG_1:29;
then ((a |^ (i2 - 1)) ` ) ` = (a ` ) \ ((a |^ (- m)) ` ) by BCIALG_1:9;
then ((a |^ (i2 - 1)) ` ) ` = (a ` ) \ (((a ` ) |^ m) ` ) by Th10;
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 A10, ABSVALUE:def 1;
then ((a |^ (i2 - 1)) ` ) ` = a |^ (i2 - 1) by A10, Def2;
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(A1, A6);
hence a |^ i in AtomSet X by A5; :: thesis: verum

end;

end;