environ
vocabularies HIDDEN, SUBSET_1, NUMBERS, PROB_1, SETLIM_1, FUNCT_1, EQREL_1, NAT_1, XXREAL_0, SETFAM_1, RELAT_1, CARD_3, TARSKI, XBOOLE_0, ARYTM_3, CARD_1, SEQM_3, ORDINAL2, SEQ_2, SETLIM_2;
notations HIDDEN, TARSKI, SUBSET_1, FUNCT_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, SETFAM_1, KURATO_0, PROB_1, SETLIM_1, XXREAL_0;
definitions TARSKI, XBOOLE_0, FUNCT_2;
theorems XBOOLE_0, XBOOLE_1, KURATO_0, SETLIM_1, CARD_3, PROB_1, NAT_1, ORDINAL1;
schemes FUNCT_2;
registrations SUBSET_1, RELSET_1, XREAL_0, ORDINAL1, FUNCT_2, NAT_1;
constructors HIDDEN, SETFAM_1, NAT_1, KURATO_0, SETLIM_1, XREAL_0, RELSET_1;
requirements HIDDEN, NUMERALS, SUBSET, ARITHM;
equalities XBOOLE_0;
expansions XBOOLE_0;
definition
let X be
set ;
let A1,
A2 be
SetSequence of
X;
existence
ex b1 being SetSequence of X st
for n being Nat holds b1 . n = (A1 . n) /\ (A2 . n)
uniqueness
for b1, b2 being SetSequence of X st ( for n being Nat holds b1 . n = (A1 . n) /\ (A2 . n) ) & ( for n being Nat holds b2 . n = (A1 . n) /\ (A2 . n) ) holds
b1 = b2
commutativity
for b1, A1, A2 being SetSequence of X st ( for n being Nat holds b1 . n = (A1 . n) /\ (A2 . n) ) holds
for n being Nat holds b1 . n = (A2 . n) /\ (A1 . n)
;
existence
ex b1 being SetSequence of X st
for n being Nat holds b1 . n = (A1 . n) \/ (A2 . n)
uniqueness
for b1, b2 being SetSequence of X st ( for n being Nat holds b1 . n = (A1 . n) \/ (A2 . n) ) & ( for n being Nat holds b2 . n = (A1 . n) \/ (A2 . n) ) holds
b1 = b2
commutativity
for b1, A1, A2 being SetSequence of X st ( for n being Nat holds b1 . n = (A1 . n) \/ (A2 . n) ) holds
for n being Nat holds b1 . n = (A2 . n) \/ (A1 . n)
;
existence
ex b1 being SetSequence of X st
for n being Nat holds b1 . n = (A1 . n) \ (A2 . n)
uniqueness
for b1, b2 being SetSequence of X st ( for n being Nat holds b1 . n = (A1 . n) \ (A2 . n) ) & ( for n being Nat holds b2 . n = (A1 . n) \ (A2 . n) ) holds
b1 = b2
existence
ex b1 being SetSequence of X st
for n being Nat holds b1 . n = (A1 . n) \+\ (A2 . n)
uniqueness
for b1, b2 being SetSequence of X st ( for n being Nat holds b1 . n = (A1 . n) \+\ (A2 . n) ) & ( for n being Nat holds b2 . n = (A1 . n) \+\ (A2 . n) ) holds
b1 = b2
commutativity
for b1, A1, A2 being SetSequence of X st ( for n being Nat holds b1 . n = (A1 . n) \+\ (A2 . n) ) holds
for n being Nat holds b1 . n = (A2 . n) \+\ (A1 . n)
;
end;