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:3;
((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:3;
a |^ (i2 - 1) = (BCI-power X) . ((a `),|.(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 `),|.(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;