environ
vocabularies HIDDEN, NUMBERS, BCIALG_1, SUBSET_1, INT_1, FUNCT_1, NAT_1, XBOOLE_0, ZFMISC_1, STRUCT_0, CARD_1, SUPINF_2, ARYTM_3, RELAT_1, NEWTON, COMPLEX1, XXREAL_0, WAYBEL15, ARYTM_1, GROUP_1, INT_2, UNIALG_2, CARD_FIL, RCOMP_1, BCIALG_2, REALSET1, MSSUBFAM, FUNCOP_1, MOD_4, GROUP_6, TARSKI, FUNCT_2, CHORD, WELLORD1, EQREL_1, CARD_3, BINOP_1, BCIALG_6, ORDINAL1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REALSET1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, XCMPLX_0, STRUCT_0, BCIALG_1, FUNCOP_1, ORDINAL1, NUMBERS, INT_2, XXREAL_0, NAT_D, INT_1, NAT_1, BCIALG_2, EQREL_1;
definitions TARSKI, BCIALG_1, FUNCT_1, XBOOLE_0;
theorems TARSKI, FUNCT_1, FUNCT_2, FUNCOP_1, ZFMISC_1, RELAT_1, XBOOLE_0, XBOOLE_1, BCIALG_1, GROUP_6, BCIALG_2, EQREL_1, RELSET_1, ABSVALUE, ORDINAL1, NAT_D, XREAL_1, INT_1, XCMPLX_1, INT_2, NAT_1, NEWTON, XXREAL_0;
schemes BINOP_1, FUNCT_2, NAT_1, INT_1, CLASSES1;
registrations RELSET_1, REALSET1, STRUCT_0, BCIALG_1, BCIALG_2, FUNCT_2, PARTFUN1, NAT_1, XREAL_0, ORDINAL1, XXREAL_0, INT_1, XCMPLX_0;
constructors HIDDEN, BINOP_1, REALSET1, BCIALG_2, REAL_1, BINOP_2, FINSEQOP, NAT_D, RELSET_1, XXREAL_0, NAT_1;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
equalities REALSET1, BINOP_1, STRUCT_0, BCIALG_1, BCIALG_2, XBOOLE_0;
expansions TARSKI, BINOP_1, BCIALG_1, XBOOLE_0;
definition
let G be non
empty BCIStr_0 ;
existence
ex b1 being Function of [: the carrier of G,NAT:], the carrier of G st
for x being Element of G holds
( b1 . (x,0) = 0. G & ( for n being Nat holds b1 . (x,(n + 1)) = x \ ((b1 . (x,n)) `) ) )
uniqueness
for b1, b2 being Function of [: the carrier of G,NAT:], the carrier of G st ( for x being Element of G holds
( b1 . (x,0) = 0. G & ( for n being Nat holds b1 . (x,(n + 1)) = x \ ((b1 . (x,n)) `) ) ) ) & ( for x being Element of G holds
( b2 . (x,0) = 0. G & ( for n being Nat holds b2 . (x,(n + 1)) = x \ ((b2 . (x,n)) `) ) ) ) holds
b1 = b2
end;
Lm1:
for X being BCI-algebra
for a being Element of AtomSet X
for m, n being Nat holds a |^ (n + m) = (a |^ m) \ ((a |^ n) `)
Lm2:
for X being BCI-algebra
for a being Element of AtomSet X
for m, n being Nat holds (a |^ m) |^ n = a |^ (m * n)
Lm3:
for X being BCI-algebra
for a being Element of AtomSet X
for i, j being Integer st i > 0 & j > 0 holds
(a |^ i) \ (a |^ j) = a |^ (i - j)
Lm4:
for X, X9 being BCI-algebra
for H9 being SubAlgebra of X9
for f being BCI-homomorphism of X,X9 st the carrier of H9 = rng f holds
f is BCI-homomorphism of X,H9
Lm5:
for X being BCI-algebra
for G being SubAlgebra of X
for K being closed Ideal of X
for RK being I-congruence of X,K
for w being Element of Union (G,RK) ex a being Element of G st w in Class (RK,a)
definition
let X be
BCI-algebra;
let G be
SubAlgebra of
X;
let K be
closed Ideal of
X;
let RK be
I-congruence of
X,
K;
existence
ex b1 being BinOp of (Union (G,RK)) st
for w1, w2 being Element of Union (G,RK)
for x, y being Element of X st w1 = x & w2 = y holds
b1 . (w1,w2) = x \ y
uniqueness
for b1, b2 being BinOp of (Union (G,RK)) st ( for w1, w2 being Element of Union (G,RK)
for x, y being Element of X st w1 = x & w2 = y holds
b1 . (w1,w2) = x \ y ) & ( for w1, w2 being Element of Union (G,RK)
for x, y being Element of X st w1 = x & w2 = y holds
b2 . (w1,w2) = x \ y ) holds
b1 = b2
end;