let Al be QC-alphabet ; :: thesis: for Al2 being Al -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)))
let Al2 be Al -expanding QC-alphabet ; :: thesis: 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)))
let p2 be Element of CQC-WFF Al2; :: thesis: 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)))
let S be CQC_Substitution of Al; :: thesis: 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)))
let S2 be CQC_Substitution of Al2; :: thesis: 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)))
let x2 be bound_QC-variable of Al2; :: thesis: 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)))
let x be bound_QC-variable of Al; :: thesis: 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)))
let p be Element of CQC-WFF Al; :: thesis: ( p = p2 & S = S2 & x = x2 implies ExpandSub (x,p,(RestrictSub (x,(All (x,p)),S))) = ExpandSub (x2,p2,(RestrictSub (x2,(All (x2,p2)),S2))) )
assume A1: ( p = p2 & S = S2 & x = x2 ) ; :: thesis: ExpandSub (x,p,(RestrictSub (x,(All (x,p)),S))) = ExpandSub (x2,p2,(RestrictSub (x2,(All (x2,p2)),S2)))
set rsub = RestrictSub (x,(All (x,p)),S);
set rsub2 = RestrictSub (x2,(All (x2,p2)),S2);
set esub = ExpandSub (x,p,(RestrictSub (x,(All (x,p)),S)));
set esub2 = ExpandSub (x2,p2,(RestrictSub (x2,(All (x2,p2)),S2)));
set uv = upVar ((RestrictSub (x,(All (x,p)),S)),p);
set uv2 = upVar ((RestrictSub (x2,(All (x2,p2)),S2)),p2);
A2: x. (upVar ((RestrictSub (x,(All (x,p)),S)),p)) = [4,(upVar ((RestrictSub (x,(All (x,p)),S)),p))] by QC_LANG3:def 2
.= [4,(upVar ((RestrictSub (x2,(All (x2,p2)),S2)),p2))] by A1, Th13, Th14
.= x. (upVar ((RestrictSub (x2,(All (x2,p2)),S2)),p2)) by QC_LANG3:def 2 ;