environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, CQC_LANG, QC_LANG1, SUBSTUT1, MCART_1, MARGREL1, REALSET1, FINSEQ_1, ORDINAL4, XBOOLEAN, CARD_1, ZFMISC_1, RELAT_1, BVFUNC_2, XBOOLE_0, FUNCT_1, TARSKI, ZF_LANG, FUNCT_4, FUNCOP_1, CLASSES2, SUBLEMMA, PARTFUN1, CQC_SIM1, ARYTM_3, XXREAL_0, ARYTM_1, SUBSTUT2, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, ORDINAL1, SUBSET_1, FINSEQ_1, FUNCT_1, QC_LANG1, QC_LANG2, QC_LANG3, PARTFUN1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, CQC_LANG, FUNCOP_1, RELAT_1, FUNCT_4, FUNCT_2, CQC_SIM1, DOMAIN_1, MCART_1, SUBSTUT1, SUBLEMMA;
definitions TARSKI;
theorems TARSKI, FUNCT_1, XBOOLE_0, XBOOLE_1, CQC_LANG, QC_LANG1, ZFMISC_1, RELAT_1, QC_LANG3, PARTFUN1, RELSET_1, QC_LANG2, SUBSTUT1, FUNCT_4, SUBLEMMA, CQC_SIM1, FUNCT_2, NAT_1, INT_1, XREAL_1, XXREAL_0, FUNCOP_1, CARD_1, XTUPLE_0;
schemes CQC_LANG, NAT_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, XREAL_0, NAT_1, INT_1, QC_LANG1, CQC_LANG, SUBSTUT1, SUBLEMMA, XTUPLE_0;
constructors HIDDEN, PARTFUN1, DOMAIN_1, XXREAL_0, NAT_1, INT_1, QC_LANG3, CQC_SIM1, SUBLEMMA, RELSET_1, XTUPLE_0, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities FUNCOP_1;
expansions TARSKI;
Lm1:
for Al being QC-alphabet
for k being Nat
for P being QC-pred_symbol of k,Al
for k, l being Nat st P is QC-pred_symbol of k,Al & P is QC-pred_symbol of l,Al holds
k = l
theorem Th9:
for
Al being
QC-alphabet for
p being
Element of
CQC-WFF Al for
x being
bound_QC-variable of
Al for
Sub being
CQC_Substitution of
Al holds
ExpandSub (
x,
p,
(RestrictSub (x,(All (x,p)),Sub)))
= (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub]))