let X be BCI-algebra; :: thesis: for x being Element of X
for a being Element of AtomSet X
for n being Nat st a = ((x `) `) |^ n holds
x |^ n in BranchV a
let x be Element of X; :: thesis: for a being Element of AtomSet X
for n being Nat st a = ((x `) `) |^ n holds
x |^ n in BranchV a
let a be Element of AtomSet X; :: thesis: for n being Nat st a = ((x `) `) |^ n holds
x |^ n in BranchV a
let n be Nat; :: thesis: ( a = ((x `) `) |^ n implies x |^ n in BranchV a )
defpred S₁[ Nat] means for a being Element of AtomSet X st a = ((x `) `) |^ $1 holds
x |^ $1 in BranchV a;

A1: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]

now :: thesis: for a being Element of AtomSet X st a = ((x `) `) |^ (n + 1) & a = ((x `) `) |^ (n + 1) holds
x |^ (n + 1) in BranchV a

set b = ((x `) `) |^ n;
let a be Element of AtomSet X; :: thesis: ( a = ((x `) `) |^ (n + 1) & a = ((x `) `) |^ (n + 1) implies x |^ (n + 1) in BranchV a )
assume a = ((x `) `) |^ (n + 1) ; :: thesis: ( a = ((x `) `) |^ (n + 1) implies x |^ (n + 1) in BranchV a )
(x `) ` in AtomSet X by BCIALG_1:34;
then reconsider b = ((x `) `) |^ n as Element of AtomSet X by Th13;
( 0. X in AtomSet X & x |^ n in BranchV b ) by A2;
then (x |^ n) ` = (((x `) `) |^ n) ` by BCIALG_1:37;
then A3: x |^ (n + 1) = x \ ((((x `) `) |^ n) `) by Th2;
((((x `) `) \ ((((x `) `) |^ n) `)) \ (x \ ((((x `) `) |^ n) `))) \ (((x `) `) \ x) = 0. X by BCIALG_1:def 3;
then ((((x `) `) |^ (n + 1)) \ (x |^ (n + 1))) \ (((x `) `) \ x) = 0. X by A3, Th2;
then ((((x `) `) |^ (n + 1)) \ (x |^ (n + 1))) \ (0. X) = 0. X by BCIALG_1:1;
then (((x `) `) |^ (n + 1)) \ (x |^ (n + 1)) = 0. X by BCIALG_1:2;
then ((x `) `) |^ (n + 1) <= x |^ (n + 1) ;
hence ( a = ((x `) `) |^ (n + 1) implies x |^ (n + 1) in BranchV a ) ; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

x |^ 0 = 0. X by Def1;
then (0. X) \ (x |^ 0) = 0. X by BCIALG_1:2;
then 0. X <= x |^ 0 ;
then ((x `) `) |^ 0 <= x |^ 0 by Def1;
then A4: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A1);
hence ( a = ((x `) `) |^ n implies x |^ n in BranchV a ) ; :: thesis: verum