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 ;

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)) )
;

end;

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;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

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;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