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 ;

per cases ( not x in rng (RestrictSub (x,(All (x,p)),S)) or x in rng (RestrictSub (x,(All (x,p)),S)) ) ;

suppose A3: not x in rng (RestrictSub (x,(All (x,p)),S)) ; :: thesis: ExpandSub (x,p,(RestrictSub (x,(All (x,p)),S))) = ExpandSub (x2,p2,(RestrictSub (x2,(All (x2,p2)),S2)))

then not x2 in rng (RestrictSub (x2,(All (x2,p2)),S2)) by A1, Th13;
hence ExpandSub (x2,p2,(RestrictSub (x2,(All (x2,p2)),S2))) = (RestrictSub (x2,(All (x2,p2)),S2)) \/ {[x2,x2]} by SUBSTUT1:def 13
.= (RestrictSub (x,(All (x,p)),S)) \/ {[x,x]} by A1, Th13
.= ExpandSub (x,p,(RestrictSub (x,(All (x,p)),S))) by A3, SUBSTUT1:def 13 ;
:: thesis: verum

end;

suppose A4: x in rng (RestrictSub (x,(All (x,p)),S)) ; :: thesis: ExpandSub (x,p,(RestrictSub (x,(All (x,p)),S))) = ExpandSub (x2,p2,(RestrictSub (x2,(All (x2,p2)),S2)))

then x2 in rng (RestrictSub (x2,(All (x2,p2)),S2)) by A1, Th13;
hence ExpandSub (x2,p2,(RestrictSub (x2,(All (x2,p2)),S2))) = (RestrictSub (x2,(All (x2,p2)),S2)) \/ {[x2,(x. (upVar ((RestrictSub (x2,(All (x2,p2)),S2)),p2)))]} by SUBSTUT1:def 13
.= (RestrictSub (x,(All (x,p)),S)) \/ {[x,(x. (upVar ((RestrictSub (x,(All (x,p)),S)),p)))]} by A1, Th13, A2
.= ExpandSub (x,p,(RestrictSub (x,(All (x,p)),S))) by A4, SUBSTUT1:def 13 ;
:: thesis: verum

end;

end;