environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, QC_LANG1, CQC_LANG, XBOOLE_0, VALUAT_1, FINSEQ_1, HENMODEL, CQC_THE1, XBOOLEAN, BVFUNC_2, FUNCT_1, ORDINAL4, CALCUL_1, ARYTM_3, RELAT_1, CARD_1, XXREAL_0, TARSKI, ZF_MODEL, REALSET1, SUBSTUT1, SUBSTUT2, ZF_LANG, ARYTM_1, CARD_3, ZFMISC_1, FINSET_1, MCART_1, NAT_1, MARGREL1, FUNCT_2, FUNCOP_1, QC_TRANS, FUNCT_4, CLASSES2, SUBLEMMA;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XXREAL_0, NAT_1, ORDINAL1, CARD_3, FINSEQ_1, FUNCT_1, QC_LANG1, QC_LANG2, QC_LANG3, NUMBERS, CQC_LANG, RELAT_1, FINSET_1, VALUAT_1, RELSET_1, FUNCT_2, CQC_SIM1, DOMAIN_1, XTUPLE_0, MCART_1, SUBSTUT1, SUBLEMMA, SUBSTUT2, CALCUL_1, CQC_THE1, GOEDELCP, MARGREL1, FUNCT_4, FUNCOP_1, HENMODEL;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, FUNCT_1, MCART_1, XBOOLE_0, XBOOLE_1, CQC_LANG, QC_LANG1, ZFMISC_1, RELAT_1, QC_LANG3, QC_LANG2, HENMODEL, CALCUL_1, SUBLEMMA, NAT_1, FINSEQ_1, VALUAT_1, FUNCT_2, SUBSTUT2, CQC_SIM1, CARD_2, ORDINAL1, CARD_1, GOEDELCP, FUNCOP_1, FINSEQ_2, FINSET_1, SUBSTUT1, FUNCT_4, CARD_4, XTUPLE_0, XXREAL_0;
schemes CQC_LANG, FINSET_1, FRAENKEL;
registrations SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, HENMODEL, FINSEQ_1, FINSET_1, CARD_3, XBOOLE_0, QC_LANG1, CQC_LANG, MARGREL1, CARD_1, GOEDELCP, FUNCOP_1, SUBLEMMA, SUBSTUT1, XTUPLE_0;
constructors HIDDEN, SETFAM_1, DOMAIN_1, XXREAL_0, NAT_1, NAT_D, FINSEQ_2, QC_LANG1, CQC_THE1, CQC_SIM1, SUBLEMMA, SUBSTUT2, CALCUL_1, HENMODEL, CARD_3, RELSET_1, CARD_1, WELLORD2, GOEDELCP, VALUAT_1, MARGREL1, CQC_LANG, QC_LANG3, FUNCT_4, FUNCOP_1, SUBSTUT1, PARTFUN1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities QC_LANG1;
expansions TARSKI, QC_LANG1;
theorem Th15:
for
Al being
QC-alphabet for
Al2 being
b1 -expanding QC-alphabet for
p2 being
Element of
CQC-WFF Al2 for
S being
CQC_Substitution of
Al for
S2 being
CQC_Substitution of
Al2 for
x2 being
bound_QC-variable of
Al2 for
x being
bound_QC-variable of
Al for
p being
Element of
CQC-WFF Al st
p = p2 &
S = S2 &
x = x2 holds
ExpandSub (
x,
p,
(RestrictSub (x,(All (x,p)),S)))
= ExpandSub (
x2,
p2,
(RestrictSub (x2,(All (x2,p2)),S2)))