let X be BCI-algebra; :: thesis: for a being Element of AtomSet X
for n, m being Nat holds a |^ (n + m) = (a |^ m) \ ((a |^ n) ` )
let a be Element of AtomSet X; :: thesis: for n, m being Nat holds a |^ (n + m) = (a |^ m) \ ((a |^ n) ` )
let n, m be Nat; :: thesis: a |^ (n + m) = (a |^ m) \ ((a |^ n) ` )
defpred S<sub>1</sub>[ Nat] means a |^ (n + $1) = (a |^ $1) \ ((a |^ n) ` );
reconsider p = a |^ n as Element of AtomSet X by Th12;
(a |^ 0 ) \ ((a |^ n) ` ) = ((a |^ n) ` ) ` by Def1
.= p by BCIALG_1:29 ;
then A1: S₁[ 0 ] ;

A3: now

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume B1: S₁[m] ; :: thesis: S₁[m + 1]
reconsider q = a |^ (m + 1) as Element of AtomSet X by Th12;
a |^ (n + (m + 1)) = a |^ ((n + m) + 1)
.= a \ (((a |^ m) \ ((a |^ n) ` )) ` ) by B1, Th1
.= a \ (((a |^ m) ` ) \ (((a |^ n) ` ) ` )) by BCIALG_1:9
.= a \ (((a |^ m) ` ) \ p) by BCIALG_1:29
.= p \ (((a |^ m) ` ) \ a) by Th0
.= (a |^ n) \ ((a |^ (m + 1)) ` ) by Th13
.= q \ (p ` ) by Th0
.= (a |^ (m + 1)) \ ((a |^ n) ` ) ;
hence S₁[m + 1] ; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A1, A3);
hence a |^ (n + m) = (a |^ m) \ ((a |^ n) ` ) ; :: thesis: verum