environ
vocabularies HIDDEN, NUMBERS, STRUCT_0, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, NAT_1, ORDINAL4, VECTSP_1, INT_3, CARD_1, SUPINF_2, MESFUNC1, ARYTM_3, INT_1, QC_LANG1, XBOOLE_0, TARSKI, BINOP_1, ZFMISC_1, RLVECT_1, ALGSTR_0, GROUP_1, RLVECT_2, XXREAL_0, CARD_3, RLVECT_3, REALSET1, VALUED_1, FINSEQ_2, PARTFUN1, FINSET_1, FUNCT_4, RLVECT_5, ORDINAL2, BSPACE;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, DOMAIN_1, RELSET_1, FUNCT_1, ORDINAL1, NUMBERS, NAT_1, INT_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_7, XXREAL_0, CARD_1, FINSET_1, FINSEQ_1, FINSEQ_2, FINSEQOP, CARD_2, STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1, VECTSP_6, VECTSP_7, MATRLIN, VECTSP_9, INT_3, RANKNULL;
definitions TARSKI, FUNCT_1, XBOOLE_0, VECTSP_1, RLVECT_1, STRUCT_0, ALGSTR_0;
theorems TARSKI, ZFMISC_1, FINSEQ_1, FUNCT_1, VECTSP_7, CARD_2, XBOOLE_1, FUNCT_2, SUBSET_1, XBOOLE_0, VECTSP_1, RLVECT_1, VECTSP_4, VECTSP_6, STRUCT_0, CARD_1, FUNCOP_1, FUNCT_7, FINSEQ_2, NAT_1, WELLORD2, RANKNULL, MATRIX_3, INT_2, INT_3, GR_CY_1, NAT_D, PARTFUN1, FINSEQ_3, MATRLIN;
schemes FINSEQ_1, FINSET_1, BINOP_1, FINSEQ_2, CLASSES1;
registrations STRUCT_0, CARD_1, FINSET_1, FINSEQ_1, SUBSET_1, XBOOLE_0, VECTSP_1, ORDINAL1, XREAL_0, INT_1, VECTSP_7, RELSET_1;
constructors HIDDEN, FINSEQOP, VECTSP_7, VECTSP_9, REALSET1, WELLORD2, NAT_D, FUNCT_7, CARD_2, RANKNULL, INT_3, GR_CY_1, RELSET_1, BINOP_2, BINOP_1;
requirements HIDDEN, NUMERALS, BOOLE, ARITHM, SUBSET, REAL;
equalities FINSEQ_1, CARD_1, VECTSP_1, STRUCT_0, FINSEQ_2, BINOP_1, INT_3, ALGSTR_0, ORDINAL1;
expansions FUNCT_1, FINSEQ_1, XBOOLE_0, VECTSP_1;
theorem
for
X,
x,
y being
set holds
(
X @ x = X @ y iff (
x in X iff
y in X ) )
theorem
for
X,
Y,
x being
set holds
(
X @ x = Y @ x iff (
x in X iff
x in Y ) )
theorem
for
X,
Y being
set holds
(
X = Y iff for
x being
object holds
X @ x = Y @ x )
Lm1:
for X being set
for a, b, c being Element of (bspace X)
for A, B, C being Subset of X st a = A & b = B & c = C holds
( a + (b + c) = A \+\ (B \+\ C) & (a + b) + c = (A \+\ B) \+\ C )
Lm2:
for X being set
for a, b being Element of Z_2
for x, y being Element of (bspace X)
for c, d being Subset of X st x = c & y = d holds
( (a * x) + (b * y) = (a \*\ c) \+\ (b \*\ d) & a * (x + y) = a \*\ (c \+\ d) & (a + b) * x = (a + b) \*\ c & (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) )