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

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

now

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) by BCIALG_1:def 11;
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 by BCIALG_1:def 11;
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