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

A3: now

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

now

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 )
set b = ((x ` ) ` ) |^ n;
((x ` ) ` ) |^ n in AtomSet X

proof

(x ` ) ` in AtomSet X by BCIALG_1:34;
hence ((x ` ) ` ) |^ n in AtomSet X by Th12; :: thesis: verum

end;

then reconsider b = ((x ` ) ` ) |^ n as Element of AtomSet X ;
B5: 0. X in AtomSet X ;
x |^ n in BranchV b by B1;
then (x |^ n) ` = (((x ` ) ` ) |^ n) ` by B5, BCIALG_1:37;
then B5: x |^ (n + 1) = x \ ((((x ` ) ` ) |^ n) ` ) by Th1;
((((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 B5, Th1;
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;

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