environ
vocabularies HIDDEN, BCIALG_1, STRUCT_0, BINOP_1, SUBSET_1, XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_5, ZFMISC_1, NUMBERS, FINSEQ_1, XXREAL_0, SUPINF_2, VECTSP_1, ALGSTR_0, RLVECT_1, ARYTM_3, SETWISEO, GROUP_1, CARD_1, NAT_1, NEWTON, POWER, FINSOP_1, ORDINAL4, BCIALG_2, TARSKI, FILTER_0, BCIALG_4;
notations HIDDEN, TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, BINOP_1, FUNCT_5, STRUCT_0, ALGSTR_0, BCIALG_1, RELAT_1, ORDINAL1, NUMBERS, XXREAL_0, FINSEQ_1, FINSOP_1, SETWISEO, FUNCT_1, FUNCT_2, FINSEQ_4, XCMPLX_0, RLVECT_1, NAT_1, BCIALG_2, VECTSP_1;
definitions STRUCT_0, BCIALG_1, RLVECT_1, ALGSTR_0;
theorems TARSKI, STRUCT_0, BCIALG_1, FINSEQ_1, FINSOP_1, SETWISEO, NAT_1, BINOP_1, BCIALG_2;
schemes BINOP_1, NAT_1, CLASSES1;
registrations BCIALG_1, RELAT_1, STRUCT_0, ORDINAL1, XXREAL_0, VECTSP_1, BCIALG_2, CARD_1, XCMPLX_0, NAT_1;
constructors HIDDEN, BINOP_1, VECTSP_2, FINSOP_1, SETWISEO, FINSEQ_4, BCIALG_2, FUNCT_5, NAT_1;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS, ARITHM;
equalities STRUCT_0, BINOP_1, BCIALG_1, FINSEQ_1, ALGSTR_0;
expansions STRUCT_0, BINOP_1, BCIALG_1;
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 )
by STRUCT_0:def 10;
Lm2:
for X being BCI-Algebra_with_Condition(S)
for x, y being Element of X holds
( (x * y) \ x <= y & ( for t being Element of X 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 X holds
( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds
t <= x * y ) ) ) holds
X is BCI-Algebra_with_Condition(S)
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
definition
let X be
BCI-Algebra_with_Condition(S);
existence
ex b1 being Function of [: the carrier of X,NAT:], the carrier of X st
for h being Element of X holds
( b1 . (h,0) = 0. X & ( for n being 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 X holds
( b1 . (h,0) = 0. X & ( for n being Nat holds b1 . (h,(n + 1)) = (b1 . (h,n)) * h ) ) ) & ( for h being Element of X holds
( b2 . (h,0) = 0. X & ( for n being Nat holds b2 . (h,(n + 1)) = (b2 . (h,n)) * h ) ) ) holds
b1 = b2
end;
Lm6:
for n being Nat
for X being BCI-Algebra_with_Condition(S) holds (0. X) |^ (n + 1) = 0. X
Lm7:
for X being BCI-Algebra_with_Condition(S)
for x, a being Element of X holds (x,a) to_power 0 = x \ (a |^ 0)
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 )
by STRUCT_0:def 10;