:: BCIALG_4 semantic presentation

begin

definition
attr c1 is strict ;
struct BCIStr_1 -> ( ( ) ( ) BCIStr_0 ) , ( ( ) ( ) ZeroStr ) ;
aggr BCIStr_1(# carrier, ExternalDiff, InternalDiff, ZeroF #) -> ( ( strict ) ( strict ) BCIStr_1 ) ;
sel ExternalDiff c1 -> ( ( Function-like V18([: the carrier of c1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of c1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ( Relation-like Function-like V18([: the carrier of c1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of c1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) BinOp of the carrier of c1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ;
end;

registration
cluster non empty strict for ( ( ) ( ) BCIStr_1 ) ;
end;

definition
let A be ( ( ) ( ) BCIStr_1 ) ;
let x, y be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
func x * y -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) equals :: BCIALG_4:def 1
 the ExternalDiff of A : ( ( ) ( ) 1-sorted ) : ( ( Function-like V18([: the carrier of A : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of A : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of A : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ( Relation-like Function-like V18([: the carrier of A : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of A : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of A : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) BinOp of the carrier of A : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) . (x : ( ( ) ( ) VectSpStr over A : ( ( ) ( ) 1-sorted ) ) ,y : ( ( Function-like V18([:x : ( ( ) ( ) VectSpStr over A : ( ( ) ( ) 1-sorted ) ) ,x : ( ( ) ( ) VectSpStr over A : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( Relation-like ) set ) ,x : ( ( ) ( ) VectSpStr over A : ( ( ) ( ) 1-sorted ) ) ) ) ( Relation-like Function-like V18([:x : ( ( ) ( ) VectSpStr over A : ( ( ) ( ) 1-sorted ) ) ,x : ( ( ) ( ) VectSpStr over A : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( Relation-like ) set ) ,x : ( ( ) ( ) VectSpStr over A : ( ( ) ( ) 1-sorted ) ) ) ) Element of bool [:[:x : ( ( ) ( ) VectSpStr over A : ( ( ) ( ) 1-sorted ) ) ,x : ( ( ) ( ) VectSpStr over A : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( Relation-like ) set ) ,x : ( ( ) ( ) VectSpStr over A : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of A : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ;
end;

definition
let IT be ( ( non empty ) ( non empty ) BCIStr_1 ) ;
attr IT is with_condition_S means :: BCIALG_4:def 2
 for x, y, z being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ;
end;

definition
func BCI_S-EXAMPLE -> ( ( ) ( ) BCIStr_1 ) equals :: BCIALG_4:def 3
 BCIStr_1(# 1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ,op2 : ( ( Function-like V18([:1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) ) ( Relation-like Function-like V18([:1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) ) Element of bool [:[:1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ,op2 : ( ( Function-like V18([:1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) ) ( Relation-like Function-like V18([:1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) ) Element of bool [:[:1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like ) set ) ,1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ,op0 : ( ( ) ( V24() V25() V26() ) Element of 1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) #) : ( ( strict ) ( strict ) BCIStr_1 ) ;
end;

registration
cluster BCI_S-EXAMPLE : ( ( ) ( ) BCIStr_1 ) -> 1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) -element strict ;
end;

registration
cluster BCI_S-EXAMPLE : ( ( ) ( non empty trivial V48() 1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) -element strict ) BCIStr_1 ) -> being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ;
end;

registration
cluster non empty being_B being_C being_I being_BCI-4 strict with_condition_S for ( ( ) ( ) BCIStr_1 ) ;
end;

definition
mode BCI-Algebra_with_Condition(S) is ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCIStr_1 ) ;
end;

definition
let X be ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ;
let x, y be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
func Condition_S (x,y) -> ( ( non empty ) ( non empty ) Subset of ) equals :: BCIALG_4:def 4
 { t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where t is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) set ) : ( ( ) ( ) Element of the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) <= y : ( ( Function-like V18([:x : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,x : ( ( ) ( ) set ) ) ) ( Relation-like Function-like V18([:x : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,x : ( ( ) ( ) set ) ) ) Element of bool [:[:x : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,x : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) } ;
end;

theorem :: BCIALG_4:1
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x, y, u, v being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in Condition_S (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) & v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in Condition_S (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ;

theorem :: BCIALG_4:2
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex a being ( ( ) ( ) Element of Condition_S (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ) st
for z being ( ( ) ( ) Element of Condition_S (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ) holds z : ( ( ) ( ) Element of Condition_S (b2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ) <= a : ( ( ) ( ) Element of Condition_S (b2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ) ;

theorem :: BCIALG_4:3
for X being ( ( non empty ) ( non empty ) BCIStr_1 ) holds
( ( X : ( ( non empty ) ( non empty ) BCIStr_1 ) is ( ( 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 ) ) holds
( (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for t being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) ) iff X : ( ( non empty ) ( non empty ) BCIStr_1 ) is ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) ;

theorem :: BCIALG_4:4
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex a being ( ( ) ( ) Element of Condition_S (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ) st
for z being ( ( ) ( ) Element of Condition_S (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ) holds z : ( ( ) ( ) Element of Condition_S (b2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ) <= a : ( ( ) ( ) Element of Condition_S (b2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ) ;

definition
let X be ( ( non empty being_B being_C being_I being_BCI-4 p-Semisimple ) ( non empty being_B being_C being_I being_BCI-4 weakly-positive-implicative p-Semisimple ) BCI-algebra) ;
func Adjoint_pGroup X -> ( ( non empty strict right_complementable Abelian add-associative right_zeroed ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) AbGroup) means :: BCIALG_4:def 5
( the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) = the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) & ( for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds the addF of it : ( ( ) ( ) set ) : ( ( Function-like V18([: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like Function-like V18([: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) . (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ ((0. X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) & 0. it : ( ( ) ( ) set ) : ( ( ) ( ) Element of the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = 0. X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) Element of the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) );
end;

theorem :: BCIALG_4: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) 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 p-Semisimple iff for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( 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 ) ) = 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) : ( ( ) ( V49(b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) V142(b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) positive nilpotent ) Element of the carrier of b1 : ( ( 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 ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_4:6
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) st X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) is p-Semisimple holds
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ ((0. X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) : ( ( ) ( V49(b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) V142(b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) positive nilpotent ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:7
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:8
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_4:9
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( (0. X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) : ( ( ) ( V49(b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) V142(b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) positive nilpotent ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) * x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * (0. X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) : ( ( ) ( V49(b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) V142(b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) positive nilpotent ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_4:10
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:11
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:12
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:13
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:14
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) <= x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:15
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) <= z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_4:16
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) <= (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) * (z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

registration
let X be ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ;
cluster the ExternalDiff of X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCIStr_1 ) : ( ( Function-like V18([: the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCIStr_1 ) : ( ( ) ( non empty ) set ) , the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCIStr_1 ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like Function-like V18([: the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCIStr_1 ) : ( ( ) ( non empty ) set ) , the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCIStr_1 ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) ) BinOp of the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) -> Function-like V18([: the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCIStr_1 ) : ( ( ) ( non empty ) set ) , the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCIStr_1 ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) commutative associative ;
end;

theorem :: BCIALG_4:17
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) holds 0. X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( V49(b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) V142(b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) positive nilpotent ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) is_a_unity_wrt the ExternalDiff of X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( Function-like V18([: the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ) ( Relation-like Function-like V18([: the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) commutative associative ) BinOp of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:18
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) holds the_unity_wrt the ExternalDiff of X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( Function-like V18([: the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ) ( Relation-like Function-like V18([: the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) commutative associative ) BinOp of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) = 0. X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( V49(b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) V142(b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) positive nilpotent ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:19
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) holds the ExternalDiff of X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( Function-like V18([: the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ) ( Relation-like Function-like V18([: the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) commutative associative ) BinOp of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) is having_a_unity ;

definition
let X be ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ;
func power X -> ( ( Function-like V18([: the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ,NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) , the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like Function-like V18([: the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ,NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) , the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) Function of [: the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ,NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) , the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) means :: BCIALG_4:def 6
 for h being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( it : ( ( ) ( ) set ) . (h : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,0 : ( ( ) ( V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) = 0. X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) Element of the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) & ( for n being ( ( ) ( V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds it : ( ( ) ( ) set ) . (h : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,(n : ( ( ) ( V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) = (it : ( ( ) ( ) set ) . (h : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,n : ( ( ) ( V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( ) Element of the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) * h : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) );
end;

definition
let X be ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
let n be ( ( ) ( V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;
func x |^ n -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) equals :: BCIALG_4:def 7
(power X : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like V18([: the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ,NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) , the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like Function-like V18([: the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ,NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) , the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) Function of [: the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ,NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like ) set ) , the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) . (x : ( ( ) ( ) set ) ,n : ( ( Function-like V18([:x : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,x : ( ( ) ( ) set ) ) ) ( Relation-like Function-like V18([:x : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,x : ( ( ) ( ) set ) ) ) Element of bool [:[:x : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,x : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: BCIALG_4:20
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ 0 : ( ( ) ( V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = 0. X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( V49(b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) V142(b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) positive nilpotent ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:21
for n being ( ( ) ( V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) )
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ (n : ( ( ) ( V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ n : ( ( ) ( V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:22
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ 1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:23
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ 2 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) 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 ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:24
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ 3 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) 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 ( ( ) ( non empty ) set ) ) * x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:25
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) holds (0. X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) : ( ( ) ( V49(b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) V142(b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) positive nilpotent ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) |^ 2 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = 0. X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( V49(b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) V142(b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) positive nilpotent ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:26
for n being ( ( ) ( V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) )
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) holds (0. X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) : ( ( ) ( V49(b2 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) V142(b2 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) positive nilpotent ) Element of the carrier of b2 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) |^ n : ( ( ) ( V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = 0. X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( V49(b2 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) V142(b2 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) ) positive nilpotent ) Element of the carrier of b2 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:27
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x, a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds ((x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) \ a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) \ a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ 3 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:28
for n being ( ( ) ( V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) )
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x, a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power n : ( ( ) ( V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ n : ( ( ) ( V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ;

definition
let X be ( ( non empty ) ( non empty ) BCIStr_1 ) ;
let F be ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of X : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) ;
func Product_S F -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) equals :: BCIALG_4:def 8
 the ExternalDiff of X : ( ( non empty ) ( non empty ) set ) : ( ( Function-like V18([: the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) , the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like Function-like V18([: the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) , the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) BinOp of the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) "**" F : ( ( ) ( ) set ) : ( ( ) ( ) Element of the carrier of X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: BCIALG_4:29
for X being ( ( non empty ) ( non empty ) BCIStr_1 )
for d being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds the ExternalDiff of X : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( Function-like V18([: the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like Function-like V18([: the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) ) BinOp of the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) "**" <*d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) = d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:30
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for F1, F2 being ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) holds Product_S (F1 : ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ^ F2 : ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (Product_S F1 : ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * (Product_S F2 : ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:31
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for F being ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) )
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds Product_S (F : ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ^ <*a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (Product_S F : ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:32
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for F being ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) )
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds Product_S (<*a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ^ F : ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * (Product_S F : ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:33
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for a1, a2 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds Product_S <*a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * a2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:34
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for a1, a2, a3 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds Product_S <*a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * a2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * a3 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:35
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x, a1, a2 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) \ a2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (Product_S <*a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:36
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for x, a1, a2, a3 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds ((x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) \ a2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) \ a3 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (Product_S <*a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) *> : ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:37
for X being ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S))
for a, b being ( ( ) ( ) Element of AtomSet X : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( non empty ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) )
for ma being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st ( for x being ( ( ) ( ) Element of BranchV a : ( ( ) ( ) Element of AtomSet b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( non empty ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( non empty ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= ma : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) holds
ex mb being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
for y being ( ( ) ( ) Element of BranchV b : ( ( ) ( ) Element of AtomSet b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( non empty ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( non empty ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) holds y : ( ( ) ( ) Element of BranchV b3 : ( ( ) ( ) Element of AtomSet b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( non empty ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( non empty ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 with_condition_S ) BCI-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) <= mb : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

registration
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 strict with_condition_S for ( ( ) ( ) BCIStr_1 ) ;
end;

definition
mode BCK-Algebra_with_Condition(S) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCI-Algebra_with_Condition(S)) ;
end;

theorem :: BCIALG_4:38
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S))
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_4:39
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S))
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds ((x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) \ (z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) = 0. X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) : ( ( ) ( V49(b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) ) V142(b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) ) positive nilpotent ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:40
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S))
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) * (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_4:41
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S))
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (0. X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) ) : ( ( ) ( V49(b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) ) V142(b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) ) positive nilpotent ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) * ((0. X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) ) : ( ( ) ( V49(b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) ) V142(b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) ) positive nilpotent ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

definition
let IT be ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) ;
attr IT is commutative means :: BCIALG_4:def 9
 for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;
end;

registration
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative for ( ( ) ( ) BCIStr_1 ) ;
end;

theorem :: BCIALG_4:42
for X being ( ( non empty ) ( non empty ) BCIStr_1 ) holds
( X : ( ( non empty ) ( non empty ) BCIStr_1 ) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative ) BCK-Algebra_with_Condition(S)) iff for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ ((0. X : ( ( non empty ) ( non empty ) BCIStr_1 ) ) : ( ( ) ( V49(b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) ) ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) = (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) & (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) BCIStr_1 ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: BCIALG_4:43
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative ) BCK-Algebra_with_Condition(S))
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is greatest holds
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ ((a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative ) BCK-Algebra_with_Condition(S)) : ( ( ) ( 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 a be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
func Initial_section a -> ( ( non empty ) ( non empty ) Subset of ) equals :: BCIALG_4:def 10
 { t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where t is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= a : ( ( ) ( ) set ) } ;
end;

theorem :: BCIALG_4:44
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative ) BCK-Algebra_with_Condition(S))
for a, b, c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st Condition_S (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) c= Initial_section c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) Subset of ) holds
for x being ( ( ) ( ) Element of Condition_S (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ) holds x : ( ( ) ( ) Element of Condition_S (b2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) Subset of ) ) <= c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ ((c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) \ b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ;

definition
let IT be ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) ;
attr IT is positive-implicative means :: BCIALG_4:def 11
 for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;
end;

registration
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S positive-implicative for ( ( ) ( ) BCIStr_1 ) ;
end;

theorem :: BCIALG_4:45
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) is positive-implicative iff for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_4:46
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) is positive-implicative iff for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_4:47
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) is positive-implicative iff for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) = (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) * (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_4:48
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) is positive-implicative iff for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_4:49
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S positive-implicative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S positive-implicative ) BCK-Algebra_with_Condition(S))
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S positive-implicative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S positive-implicative ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) * (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S positive-implicative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S positive-implicative ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S positive-implicative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S positive-implicative ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

definition
let IT be ( ( non empty ) ( non empty ) BCIStr_1 ) ;
attr IT is being_SB-1 means :: BCIALG_4:def 12
 for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
attr IT is being_SB-2 means :: BCIALG_4:def 13
 for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
attr IT is being_SB-4 means :: BCIALG_4:def 14
 for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
end;

registration
cluster BCI_S-EXAMPLE : ( ( ) ( non empty trivial V48() 1 : ( ( ) ( non empty V24() V25() V26() V30() V33() V38() ext-real ) Element of NAT : ( ( ) ( non empty V24() V25() V26() V33() V38() V39() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) -element being_B being_C being_I being_BCI-4 being_BCK-5 strict with_condition_S ) BCIStr_1 ) -> being_I with_condition_S being_SB-1 being_SB-2 being_SB-4 ;
end;

registration
cluster non empty being_I strict with_condition_S being_SB-1 being_SB-2 being_SB-4 for ( ( ) ( ) BCIStr_1 ) ;
end;

definition
mode semi-Brouwerian-algebra is ( ( non empty being_I with_condition_S being_SB-1 being_SB-2 being_SB-4 ) ( non empty being_I with_condition_S being_SB-1 being_SB-2 being_SB-4 ) BCIStr_1 ) ;
end;

theorem :: BCIALG_4:50
for X being ( ( non empty ) ( non empty ) BCIStr_1 ) holds
( X : ( ( non empty ) ( non empty ) BCIStr_1 ) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S positive-implicative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S positive-implicative ) BCK-Algebra_with_Condition(S)) iff X : ( ( non empty ) ( non empty ) BCIStr_1 ) is ( ( non empty being_I with_condition_S being_SB-1 being_SB-2 being_SB-4 ) ( non empty being_I with_condition_S being_SB-1 being_SB-2 being_SB-4 ) semi-Brouwerian-algebra) ) ;

definition
let IT be ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) ;
attr IT is implicative means :: BCIALG_4:def 15
 for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
end;

registration
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S implicative for ( ( ) ( ) BCIStr_1 ) ;
end;

theorem :: BCIALG_4:51
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) is implicative iff ( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) is commutative & X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) is positive-implicative ) ) ;

theorem :: BCIALG_4:52
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) is implicative iff for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) = ((x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) * (z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ) BCK-Algebra_with_Condition(S)) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;