begin
:: deftheorem defines * BCIALG_4:def 1 :
:: deftheorem Def2 defines with_condition_S BCIALG_4:def 2 :
:: deftheorem defines BCI_S-EXAMPLE BCIALG_4:def 3 :
Lm1:
( BCI_S-EXAMPLE is being_B & BCI_S-EXAMPLE is being_C & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is being_BCI-4 & BCI_S-EXAMPLE is being_BCK-5 & BCI_S-EXAMPLE is with_condition_S )
:: deftheorem defines Condition_S BCIALG_4:def 4 :
theorem
theorem
Lm2:
for X being BCI-Algebra_with_Condition(S)
for x, y being Element of holds
( (x * y) \ x <= y & ( for t being Element of st t \ x <= y holds
t <= x * y ) )
Lm3:
for X being non empty BCIStr_1 st X is BCI-algebra & ( for x, y being Element of holds
( (x * y) \ x <= y & ( for t being Element of st t \ x <= y holds
t <= x * y ) ) ) holds
X is BCI-Algebra_with_Condition(S)
theorem
theorem
:: deftheorem defines Adjoint_pGroup BCIALG_4:def 5 :
theorem Th5:
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem
theorem
Lm4:
for X being BCI-Algebra_with_Condition(S) holds the ExternalDiff of X is commutative
Lm5:
for X being BCI-Algebra_with_Condition(S) holds the ExternalDiff of X is associative
theorem Th17:
theorem
theorem Th19:
definition
let X be
BCI-Algebra_with_Condition(S);
func power X -> Function of
[:the carrier of X,NAT :],the
carrier of
X means :
Def6:
for
h being
Element of holds
(
it . h,
0 = 0. X & ( for
n being
Element of
NAT holds
it . h,
(n + 1) = (it . h,n) * h ) );
existence
ex b1 being Function of [:the carrier of X,NAT :],the carrier of X st
for h being Element of holds
( b1 . h,0 = 0. X & ( for n being Element of NAT holds b1 . h,(n + 1) = (b1 . h,n) * h ) )
uniqueness
for b1, b2 being Function of [:the carrier of X,NAT :],the carrier of X st ( for h being Element of holds
( b1 . h,0 = 0. X & ( for n being Element of NAT holds b1 . h,(n + 1) = (b1 . h,n) * h ) ) ) & ( for h being Element of holds
( b2 . h,0 = 0. X & ( for n being Element of NAT holds b2 . h,(n + 1) = (b2 . h,n) * h ) ) ) holds
b1 = b2
end;
:: deftheorem Def6 defines power BCIALG_4:def 6 :
:: deftheorem defines |^ BCIALG_4:def 7 :
theorem
theorem
theorem Th22:
theorem Th23:
theorem
theorem Th25:
Lm6:
for n being Element of NAT
for X being BCI-Algebra_with_Condition(S) holds (0. X) |^ (n + 1) = 0. X
theorem
theorem
Lm7:
for X being BCI-Algebra_with_Condition(S)
for x, a being Element of holds x,a to_power 0 = x \ (a |^ 0 )
theorem
:: deftheorem defines Product_S BCIALG_4:def 8 :
theorem
theorem
theorem
theorem
theorem Th33:
theorem Th34:
theorem
theorem
theorem
theorem Th38:
theorem
theorem
theorem
:: deftheorem Def9 defines commutative BCIALG_4:def 9 :
theorem
theorem
:: deftheorem defines Initial_section BCIALG_4:def 10 :
theorem
:: deftheorem Def11 defines positive-implicative BCIALG_4:def 11 :
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
:: deftheorem Def12 defines being_SB-1 BCIALG_4:def 12 :
:: deftheorem Def13 defines being_SB-2 BCIALG_4:def 13 :
:: deftheorem Def14 defines being_SB-4 BCIALG_4:def 14 :
Lm8:
( BCI_S-EXAMPLE is being_SB-1 & BCI_S-EXAMPLE is being_SB-2 & BCI_S-EXAMPLE is being_SB-4 & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is with_condition_S )
theorem
:: deftheorem Def15 defines implicative BCIALG_4:def 15 :
theorem Th51:
theorem