BCIALG

:: BCIALG_6 semantic presentation

begin

definition

let D be ( ( ) ( ) set ) ;
let f be ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined D : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,D : ( ( ) ( ) set ) ) ;
let n be ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) ;
:: original: .
redefine func f . n -> ( ( ) ( ) Element of D : ( ( ) ( ) BCIStr_0 ) ) ;

end;

definition

let G be ( ( non empty ) ( non empty ) BCIStr_0 ) ;

func BCI-power G -> ( ( Function-like quasi_total ) ( Relation-like [: the carrier of G : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ,NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined the carrier of G : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) -valued Function-like V14([: the carrier of G : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ,NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) ) quasi_total ) Function of [: the carrier of G : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ,NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) means :: BCIALG_6:def 1
for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( it : ( ( Function-like quasi_total ) ( Relation-like [:G : ( ( ) ( ) BCIStr_0 ) ,G : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined G : ( ( ) ( ) BCIStr_0 ) -valued Function-like quasi_total ) Element of bool [:[:G : ( ( ) ( ) BCIStr_0 ) ,G : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,0 : ( ( ) ( empty V24() V25() V26() V28() V29() V30() V92() V93() integer ext-real non positive non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of G : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) = 0. G : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( V47(G : ( ( ) ( ) BCIStr_0 ) ) ) Element of the carrier of G : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) & ( for n being ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds it : ( ( Function-like quasi_total ) ( Relation-like [:G : ( ( ) ( ) BCIStr_0 ) ,G : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined G : ( ( ) ( ) BCIStr_0 ) -valued Function-like quasi_total ) Element of bool [:[:G : ( ( ) ( ) BCIStr_0 ) ,G : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,(n : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of G : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ ((it : ( ( Function-like quasi_total ) ( Relation-like [:G : ( ( ) ( ) BCIStr_0 ) ,G : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined G : ( ( ) ( ) BCIStr_0 ) -valued Function-like quasi_total ) Element of bool [:[:G : ( ( ) ( ) BCIStr_0 ) ,G : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,n : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( ) Element of the carrier of G : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) `) : ( ( ) ( ) Element of the carrier of G : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of G : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) ) );

end;

definition

let X be ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ;
let i be ( ( integer ) ( V92() V93() integer ext-real ) Integer) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

func x |^ i -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) equals :: BCIALG_6:def 2
(BCI-power X : ( ( ) ( ) BCIStr_0 ) ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ,NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) -valued Function-like V14([: the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ,NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) ) quasi_total ) Function of [: the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ,NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) . (x : ( ( ) ( ) Element of X : ( ( ) ( ) BCIStr_0 ) ) ,(abs i : ( ( Function-like quasi_total ) ( Relation-like [:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) BCIStr_0 ) -valued Function-like quasi_total ) Element of bool [:[:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) if 0 : ( ( ) ( empty V24() V25() V26() V28() V29() V30() V92() V93() integer ext-real non positive non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) <= i : ( ( Function-like quasi_total ) ( Relation-like [:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) BCIStr_0 ) -valued Function-like quasi_total ) Element of bool [:[:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) )
otherwise (BCI-power X : ( ( ) ( ) BCIStr_0 ) ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ,NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) -valued Function-like V14([: the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ,NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) ) quasi_total ) Function of [: the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ,NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) . ((x : ( ( ) ( ) Element of X : ( ( ) ( ) BCIStr_0 ) ) `) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) ,(abs i : ( ( Function-like quasi_total ) ( Relation-like [:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) BCIStr_0 ) -valued Function-like quasi_total ) Element of bool [:[:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) ;

end;

definition

let X be ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ;
let n be ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

redefine func x |^ n equals :: BCIALG_6:def 3
(BCI-power X : ( ( ) ( ) BCIStr_0 ) ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ,NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) -defined the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) -valued Function-like V14([: the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ,NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) ) quasi_total ) Function of [: the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ,NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) , the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) . (x : ( ( ) ( ) Element of X : ( ( ) ( ) BCIStr_0 ) ) ,n : ( ( Function-like quasi_total ) ( Relation-like [:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) BCIStr_0 ) -valued Function-like quasi_total ) Element of bool [:[:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ;

end;

theorem :: BCIALG_6:1

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for a, b being ( ( ) ( ) Element of AtomSet X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) holds a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ b : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_6:2

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n being ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ (n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) + 1 : ( ( ) ( non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ ((x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_6:3

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ 0 : ( ( ) ( empty V24() V25() V26() V28() V29() V30() V92() V93() integer ext-real non positive non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = 0. X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( V47(b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) atom positive nilpotent ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_6:4

theorem :: BCIALG_6:5

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ (- 1 : ( ( ) ( non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V92() V93() integer ext-real non positive ) Element of INT : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_6:6

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ 2 : ( ( ) ( non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_6:7

theorem :: BCIALG_6:8

theorem :: BCIALG_6:9

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n being ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ (- n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) ) : ( ( ) ( V92() V93() integer ext-real non positive ) Element of INT : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = ((x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) |^ (- n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) ) : ( ( ) ( V92() V93() integer ext-real non positive ) Element of INT : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_6:10

theorem :: BCIALG_6:11

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n being ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in BCK-part X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) & n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) >= 1 : ( ( ) ( non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_6:12

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n being ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in BCK-part X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ (- n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) ) : ( ( ) ( V92() V93() integer ext-real non positive ) Element of INT : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = 0. X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( V47(b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) atom positive nilpotent ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_6:13

theorem :: BCIALG_6:14

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for a being ( ( ) ( ) Element of AtomSet X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) )
for n being ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) holds (a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) |^ (n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) + 1 : ( ( ) ( non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) = ((a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) |^ n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) \ a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_6:15

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for a, b being ( ( ) ( ) Element of AtomSet X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) )
for n being ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) holds (a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) \ b : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) |^ n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) |^ n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (b : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) |^ n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_6:16

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for a, b being ( ( ) ( ) Element of AtomSet X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) )
for n being ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) holds (a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) \ b : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) |^ (- n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) ) : ( ( ) ( V92() V93() integer ext-real non positive ) Element of INT : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) |^ (- n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) ) : ( ( ) ( V92() V93() integer ext-real non positive ) Element of INT : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (b : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) |^ (- n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) ) : ( ( ) ( V92() V93() integer ext-real non positive ) Element of INT : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_6:17

theorem :: BCIALG_6:18

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n being ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) |^ n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_6:19

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for a being ( ( ) ( ) Element of AtomSet X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) )
for n being ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) holds (a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) |^ (- n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) ) : ( ( ) ( V92() V93() integer ext-real non positive ) Element of INT : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) |^ (- n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) ) : ( ( ) ( V92() V93() integer ext-real non positive ) Element of INT : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_6:20

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( ) Element of AtomSet X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) )
for n being ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) st a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) = ((x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) |^ n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in BranchV a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;

theorem :: BCIALG_6:21

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n being ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) = (((x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) |^ n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_6:22

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for a being ( ( ) ( ) Element of AtomSet X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) )
for i, j being ( ( integer ) ( V92() V93() integer ext-real ) Integer) holds (a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) |^ i : ( ( integer ) ( V92() V93() integer ext-real ) Integer) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) |^ j : ( ( integer ) ( V92() V93() integer ext-real ) Integer) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) = a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) |^ (i : ( ( integer ) ( V92() V93() integer ext-real ) Integer) - j : ( ( integer ) ( V92() V93() integer ext-real ) Integer) ) : ( ( ) ( V92() V93() integer ext-real ) Element of INT : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_6:23

theorem :: BCIALG_6:24

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for a being ( ( ) ( ) Element of AtomSet X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) )
for i, j being ( ( integer ) ( V92() V93() integer ext-real ) Integer) holds a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) |^ (i : ( ( integer ) ( V92() V93() integer ext-real ) Integer) + j : ( ( integer ) ( V92() V93() integer ext-real ) Integer) ) : ( ( ) ( V92() V93() integer ext-real ) Element of INT : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) |^ i : ( ( integer ) ( V92() V93() integer ext-real ) Integer) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ ((a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) |^ j : ( ( integer ) ( V92() V93() integer ext-real ) Integer) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ;

definition

let X be ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

attr x is finite-period means :: BCIALG_6:def 4
ex n being ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) st
( n : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) <> 0 : ( ( ) ( empty V24() V25() V26() V28() V29() V30() V92() V93() integer ext-real non positive non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) & x : ( ( Function-like quasi_total ) ( Relation-like [:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) BCIStr_0 ) -valued Function-like quasi_total ) Element of bool [:[:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) |^ n : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in BCK-part X : ( ( ) ( ) BCIStr_0 ) : ( ( non empty ) ( non empty ) Element of bool the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) );

end;

theorem :: BCIALG_6:25

definition

let X be ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
assume x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is finite-period ;

func ord x -> ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) means :: BCIALG_6:def 5
( x : ( ( Function-like quasi_total ) ( Relation-like [:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) BCIStr_0 ) -valued Function-like quasi_total ) Element of bool [:[:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) |^ it : ( ( ) ( ) Element of X : ( ( ) ( ) BCIStr_0 ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in BCK-part X : ( ( ) ( ) BCIStr_0 ) : ( ( non empty ) ( non empty ) Element of bool the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) & it : ( ( ) ( ) Element of X : ( ( ) ( ) BCIStr_0 ) ) <> 0 : ( ( ) ( empty V24() V25() V26() V28() V29() V30() V92() V93() integer ext-real non positive non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) & ( for m being ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) st x : ( ( Function-like quasi_total ) ( Relation-like [:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) BCIStr_0 ) -valued Function-like quasi_total ) Element of bool [:[:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) |^ m : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in BCK-part X : ( ( ) ( ) BCIStr_0 ) : ( ( non empty ) ( non empty ) Element of bool the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) & m : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) <> 0 : ( ( ) ( empty V24() V25() V26() V28() V29() V30() V92() V93() integer ext-real non positive non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
it : ( ( ) ( ) Element of X : ( ( ) ( ) BCIStr_0 ) ) <= m : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) );

end;

theorem :: BCIALG_6:26

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for a being ( ( ) ( ) Element of AtomSet X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) )
for n being ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) st a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) is finite-period & ord a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) holds
a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) |^ n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = 0. X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( V47(b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) atom positive nilpotent ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_6:27

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) iff for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is finite-period & ord x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = 1 : ( ( ) ( non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) ) ;

theorem :: BCIALG_6:28

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( ) Element of AtomSet X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is finite-period & a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) is finite-period & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in BranchV a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) holds
ord x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = ord a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: BCIALG_6:29

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n, m being ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is finite-period & ord x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ m : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in BCK-part X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) iff n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) divides m : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) ) ;

theorem :: BCIALG_6:30

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for m, n being ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is finite-period & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ m : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is finite-period & ord x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) & m : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) > 0 : ( ( ) ( empty V24() V25() V26() V28() V29() V30() V92() V93() integer ext-real non positive non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
ord (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ m : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) div (m : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) gcd n : ( ( V30() ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Nat) ) : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( integer ) ( V92() V93() integer ext-real ) set ) ;

theorem :: BCIALG_6:31

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is finite-period & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) is finite-period holds
ord x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = ord (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: BCIALG_6:32

theorem :: BCIALG_6:33

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for a, b being ( ( ) ( ) Element of AtomSet X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) st a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) \ b : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) is finite-period & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is finite-period & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is finite-period & a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) is finite-period & b : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) is finite-period & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in BranchV a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in BranchV b : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) holds
ord (a : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) \ b : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of AtomSet b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) divides (ord x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) lcm (ord y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V24() V25() V26() V30() V92() V93() integer ext-real non negative ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;

begin

theorem :: BCIALG_6:34

for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra)
for Y being ( ( ) ( non empty being_B being_C being_I being_BCI-4 ) SubAlgebra of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for x9, y9 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = y9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) = x9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( ) ( non empty being_B being_C being_I being_BCI-4 ) SubAlgebra of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) : ( ( ) ( non empty ) set ) ) ;

definition

let X, X9 be ( ( non empty ) ( non empty ) BCIStr_0 ) ;
let f be ( ( Function-like quasi_total ) ( Relation-like the carrier of X : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) -defined the carrier of X9 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of X : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;

attr f is multiplicative means :: BCIALG_6:def 6
for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds f : ( ( ) ( ) Element of X : ( ( ) ( ) BCIStr_0 ) ) . (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of X9 : ( ( Function-like quasi_total ) ( Relation-like [:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) BCIStr_0 ) -valued Function-like quasi_total ) Element of bool [:[:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = (f : ( ( ) ( ) Element of X : ( ( ) ( ) BCIStr_0 ) ) . a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of X9 : ( ( Function-like quasi_total ) ( Relation-like [:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) BCIStr_0 ) -valued Function-like quasi_total ) Element of bool [:[:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) \ (f : ( ( ) ( ) Element of X : ( ( ) ( ) BCIStr_0 ) ) . b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of X9 : ( ( Function-like quasi_total ) ( Relation-like [:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) BCIStr_0 ) -valued Function-like quasi_total ) Element of bool [:[:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of X9 : ( ( Function-like quasi_total ) ( Relation-like [:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) BCIStr_0 ) -valued Function-like quasi_total ) Element of bool [:[:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

end;

registration

let X, X9 be ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ;

cluster Relation-like the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) -defined the carrier of X9 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) quasi_total multiplicative for ( ( ) ( ) Element of bool [: the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) , the carrier of X9 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

end;

definition

end;

definition

attr f is isotonic means :: BCIALG_6:def 7
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
f : ( ( ) ( ) Element of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of X9 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) <= f : ( ( ) ( ) Element of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) . y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of X9 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) ;

end;

definition

end;

definition

func Ker f -> ( ( ) ( ) set ) equals :: BCIALG_6:def 8
{ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where x is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : f : ( ( ) ( ) Element of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of X9 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) = 0. X9 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( V47(X9 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) atom positive nilpotent ) Element of the carrier of X9 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) } ;

end;

theorem :: BCIALG_6:35

registration

cluster Ker f : ( ( Function-like quasi_total multiplicative ) ( Relation-like the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) -defined the carrier of X9 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) quasi_total multiplicative ) Element of bool [: the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) , the carrier of X9 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -> non empty ;

end;

theorem :: BCIALG_6:36

theorem :: BCIALG_6:37

theorem :: BCIALG_6:38

theorem :: BCIALG_6:39

theorem :: BCIALG_6:40

theorem :: BCIALG_6:41

registration

end;

theorem :: BCIALG_6:42

theorem :: BCIALG_6:43

theorem :: BCIALG_6:44

theorem :: BCIALG_6:45

theorem :: BCIALG_6:46

theorem :: BCIALG_6:47

theorem :: BCIALG_6:48

definition

let X, X9 be ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ;

end;

registration

end;

definition

end;

begin

theorem :: BCIALG_6:49

theorem :: BCIALG_6:50

theorem :: BCIALG_6:51

theorem :: BCIALG_6:52

begin

theorem :: BCIALG_6:53

theorem :: BCIALG_6:54

begin

definition

func Union (G,RK) -> ( ( non empty ) ( non empty ) Subset of ) equals :: BCIALG_6:def 11
union { (Class (RK : ( ( ) ( ) set ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of bool the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) where a is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : Class (RK : ( ( ) ( ) set ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) in the carrier of (X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ./. RK : ( ( ) ( ) set ) ) : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) } : ( ( ) ( ) set ) ;

end;

definition

func HKOp (G,RK) -> ( ( Function-like quasi_total ) ( Relation-like [:(Union (G : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,RK : ( ( ) ( ) set ) )) : ( ( non empty ) ( non empty ) Subset of ) ,(Union (G : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,RK : ( ( ) ( ) set ) )) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( ) set ) -defined Union (G : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,RK : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V14([:(Union (G : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,RK : ( ( ) ( ) set ) )) : ( ( non empty ) ( non empty ) Subset of ) ,(Union (G : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,RK : ( ( ) ( ) set ) )) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( ) set ) ) quasi_total ) BinOp of Union (G : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,RK : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Subset of ) ) means :: BCIALG_6:def 12
for w1, w2 being ( ( ) ( ) Element of Union (G : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,RK : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Subset of ) )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st w1 : ( ( ) ( ) Element of Union (G : ( ( ) ( non empty being_B being_C being_I being_BCI-4 ) SubAlgebra of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ,RK : ( ( ) ( Relation-like the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) -defined the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) -valued V14( the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) quasi_total V77() V79() V84() ) I-congruence of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ,K : ( ( closed ) ( non empty closed ) Ideal of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & w2 : ( ( ) ( ) Element of Union (G : ( ( ) ( non empty being_B being_C being_I being_BCI-4 ) SubAlgebra of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ,RK : ( ( ) ( Relation-like the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) -defined the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) -valued V14( the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) quasi_total V77() V79() V84() ) I-congruence of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ,K : ( ( closed ) ( non empty closed ) Ideal of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
it : ( ( ) ( ) Element of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) . (w1 : ( ( ) ( ) Element of Union (G : ( ( ) ( non empty being_B being_C being_I being_BCI-4 ) SubAlgebra of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ,RK : ( ( ) ( Relation-like the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) -defined the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) -valued V14( the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) quasi_total V77() V79() V84() ) I-congruence of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ,K : ( ( closed ) ( non empty closed ) Ideal of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ) ,w2 : ( ( ) ( ) Element of Union (G : ( ( ) ( non empty being_B being_C being_I being_BCI-4 ) SubAlgebra of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ,RK : ( ( ) ( Relation-like the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) -defined the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) -valued V14( the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) quasi_total V77() V79() V84() ) I-congruence of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ,K : ( ( closed ) ( non empty closed ) Ideal of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ) ) : ( ( ) ( ) Element of Union (G : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,RK : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Subset of ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) ;

end;

definition

end;

definition

func HK (G,RK) -> ( ( ) ( ) BCIStr_0 ) equals :: BCIALG_6:def 14
BCIStr_0(# (Union (G : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,RK : ( ( ) ( ) set ) )) : ( ( non empty ) ( non empty ) Subset of ) ,(HKOp (G : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,RK : ( ( ) ( ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like [:(Union (G : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,RK : ( ( ) ( ) set ) )) : ( ( non empty ) ( non empty ) Subset of ) ,(Union (G : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,RK : ( ( ) ( ) set ) )) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( ) set ) -defined Union (G : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,RK : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V14([:(Union (G : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,RK : ( ( ) ( ) set ) )) : ( ( non empty ) ( non empty ) Subset of ) ,(Union (G : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,RK : ( ( ) ( ) set ) )) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( ) set ) ) quasi_total ) BinOp of Union (G : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,RK : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Subset of ) ) ,(zeroHK (G : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,RK : ( ( ) ( ) set ) )) : ( ( ) ( ) Element of Union (G : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,RK : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Subset of ) ) #) : ( ( strict ) ( strict ) BCIStr_0 ) ;

end;

registration

end;

definition

end;

theorem :: BCIALG_6:55

registration

end;

theorem :: BCIALG_6:56

theorem :: BCIALG_6:57

theorem :: BCIALG_6:58