let Al be QC-alphabet ; :: thesis: for Al2 being Al -expanding QC-alphabet

for Z being Element of CQC-Sub-WFF Al

for Z2 being Element of CQC-Sub-WFF Al2 st Z `1 is universal & Z2 `1 is universal & bound_in (Z `1) = bound_in (Z2 `1) & the_scope_of (Z `1) = the_scope_of (Z2 `1) & Z = Z2 holds

S_Bound (@ Z) = S_Bound (@ Z2)

let Al2 be Al -expanding QC-alphabet ; :: thesis: for Z being Element of CQC-Sub-WFF Al

for Z2 being Element of CQC-Sub-WFF Al2 st Z `1 is universal & Z2 `1 is universal & bound_in (Z `1) = bound_in (Z2 `1) & the_scope_of (Z `1) = the_scope_of (Z2 `1) & Z = Z2 holds

S_Bound (@ Z) = S_Bound (@ Z2)

let Z be Element of CQC-Sub-WFF Al; :: thesis: for Z2 being Element of CQC-Sub-WFF Al2 st Z `1 is universal & Z2 `1 is universal & bound_in (Z `1) = bound_in (Z2 `1) & the_scope_of (Z `1) = the_scope_of (Z2 `1) & Z = Z2 holds

S_Bound (@ Z) = S_Bound (@ Z2)

let Z2 be Element of CQC-Sub-WFF Al2; :: thesis: ( Z `1 is universal & Z2 `1 is universal & bound_in (Z `1) = bound_in (Z2 `1) & the_scope_of (Z `1) = the_scope_of (Z2 `1) & Z = Z2 implies S_Bound (@ Z) = S_Bound (@ Z2) )

assume A1: ( Z `1 is universal & Z2 `1 is universal & bound_in (Z `1) = bound_in (Z2 `1) & the_scope_of (Z `1) = the_scope_of (Z2 `1) & Z = Z2 ) ; :: thesis: S_Bound (@ Z) = S_Bound (@ Z2)

set p = (@ Z) `1 ;

set p2 = (@ Z2) `1 ;

set S = (@ Z) `2 ;

set S2 = (@ Z2) `2 ;

reconsider p = (@ Z) `1 as Element of CQC-WFF Al by A1, SUBSTUT1:def 35;

reconsider p2 = (@ Z2) `1 as Element of CQC-WFF Al2 by A1, SUBSTUT1:def 35;

reconsider S = (@ Z) `2 as CQC_Substitution of Al ;

reconsider S2 = (@ Z2) `2 as CQC_Substitution of Al2 ;

set x = bound_in p;

set x2 = bound_in p2;

set q = the_scope_of p;

set q2 = the_scope_of p2;

p is universal by A1, SUBSTUT1:def 35;

then p = All ((bound_in p),(the_scope_of p)) by QC_LANG2:6;

then reconsider q = the_scope_of p as Element of CQC-WFF Al by CQC_LANG:13;

p2 is universal by A1, SUBSTUT1:def 35;

then p2 = All ((bound_in p2),(the_scope_of p2)) by QC_LANG2:6;

then reconsider q2 = the_scope_of p2 as Element of CQC-WFF Al2 by CQC_LANG:13;

reconsider x = bound_in p as bound_QC-variable of Al ;

reconsider x2 = bound_in p2 as bound_QC-variable of Al2 ;

A2: p = Z `1 by SUBSTUT1:def 35

.= p2 by A1, SUBSTUT1:def 35 ;

A3: S = Z `2 by SUBSTUT1:def 35

.= S2 by A1, SUBSTUT1:def 35 ;

A4: x = bound_in (Z `1) by SUBSTUT1:def 35

.= x2 by A1, SUBSTUT1:def 35 ;

A5: q = the_scope_of (Z `1) by SUBSTUT1:def 35

.= q2 by A1, SUBSTUT1:def 35 ;

set rsub = RestrictSub (x,p,S);

set rsub2 = RestrictSub (x2,p2,S2);

for Z being Element of CQC-Sub-WFF Al

for Z2 being Element of CQC-Sub-WFF Al2 st Z `1 is universal & Z2 `1 is universal & bound_in (Z `1) = bound_in (Z2 `1) & the_scope_of (Z `1) = the_scope_of (Z2 `1) & Z = Z2 holds

S_Bound (@ Z) = S_Bound (@ Z2)

let Al2 be Al -expanding QC-alphabet ; :: thesis: for Z being Element of CQC-Sub-WFF Al

for Z2 being Element of CQC-Sub-WFF Al2 st Z `1 is universal & Z2 `1 is universal & bound_in (Z `1) = bound_in (Z2 `1) & the_scope_of (Z `1) = the_scope_of (Z2 `1) & Z = Z2 holds

S_Bound (@ Z) = S_Bound (@ Z2)

let Z be Element of CQC-Sub-WFF Al; :: thesis: for Z2 being Element of CQC-Sub-WFF Al2 st Z `1 is universal & Z2 `1 is universal & bound_in (Z `1) = bound_in (Z2 `1) & the_scope_of (Z `1) = the_scope_of (Z2 `1) & Z = Z2 holds

S_Bound (@ Z) = S_Bound (@ Z2)

let Z2 be Element of CQC-Sub-WFF Al2; :: thesis: ( Z `1 is universal & Z2 `1 is universal & bound_in (Z `1) = bound_in (Z2 `1) & the_scope_of (Z `1) = the_scope_of (Z2 `1) & Z = Z2 implies S_Bound (@ Z) = S_Bound (@ Z2) )

assume A1: ( Z `1 is universal & Z2 `1 is universal & bound_in (Z `1) = bound_in (Z2 `1) & the_scope_of (Z `1) = the_scope_of (Z2 `1) & Z = Z2 ) ; :: thesis: S_Bound (@ Z) = S_Bound (@ Z2)

set p = (@ Z) `1 ;

set p2 = (@ Z2) `1 ;

set S = (@ Z) `2 ;

set S2 = (@ Z2) `2 ;

reconsider p = (@ Z) `1 as Element of CQC-WFF Al by A1, SUBSTUT1:def 35;

reconsider p2 = (@ Z2) `1 as Element of CQC-WFF Al2 by A1, SUBSTUT1:def 35;

reconsider S = (@ Z) `2 as CQC_Substitution of Al ;

reconsider S2 = (@ Z2) `2 as CQC_Substitution of Al2 ;

set x = bound_in p;

set x2 = bound_in p2;

set q = the_scope_of p;

set q2 = the_scope_of p2;

p is universal by A1, SUBSTUT1:def 35;

then p = All ((bound_in p),(the_scope_of p)) by QC_LANG2:6;

then reconsider q = the_scope_of p as Element of CQC-WFF Al by CQC_LANG:13;

p2 is universal by A1, SUBSTUT1:def 35;

then p2 = All ((bound_in p2),(the_scope_of p2)) by QC_LANG2:6;

then reconsider q2 = the_scope_of p2 as Element of CQC-WFF Al2 by CQC_LANG:13;

reconsider x = bound_in p as bound_QC-variable of Al ;

reconsider x2 = bound_in p2 as bound_QC-variable of Al2 ;

A2: p = Z `1 by SUBSTUT1:def 35

.= p2 by A1, SUBSTUT1:def 35 ;

A3: S = Z `2 by SUBSTUT1:def 35

.= S2 by A1, SUBSTUT1:def 35 ;

A4: x = bound_in (Z `1) by SUBSTUT1:def 35

.= x2 by A1, SUBSTUT1:def 35 ;

A5: q = the_scope_of (Z `1) by SUBSTUT1:def 35

.= q2 by A1, SUBSTUT1:def 35 ;

set rsub = RestrictSub (x,p,S);

set rsub2 = RestrictSub (x2,p2,S2);

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

end;

suppose A6:
not x in rng (RestrictSub (x,p,S))
; :: thesis: S_Bound (@ Z) = S_Bound (@ Z2)

then
not x2 in rng (RestrictSub (x2,p2,S2))
by A2, A3, A4, Th13;

hence S_Bound (@ Z2) = x2 by SUBSTUT1:def 36

.= S_Bound (@ Z) by A4, A6, SUBSTUT1:def 36 ;

:: thesis: verum

end;hence S_Bound (@ Z2) = x2 by SUBSTUT1:def 36

.= S_Bound (@ Z) by A4, A6, SUBSTUT1:def 36 ;

:: thesis: verum

suppose A7:
x in rng (RestrictSub (x,p,S))
; :: thesis: S_Bound (@ Z) = S_Bound (@ Z2)

then
x2 in rng (RestrictSub (x2,p2,S2))
by A2, A3, A4, Th13;

then S_Bound (@ Z2) = x. (upVar ((RestrictSub (x2,p2,S2)),q2)) by SUBSTUT1:def 36

.= [4,(upVar ((RestrictSub (x2,p2,S2)),q2))] by QC_LANG3:def 2

.= [4,(upVar ((RestrictSub (x,p,S)),q))] by A5, A2, A3, A4, Th13, Th14

.= x. (upVar ((RestrictSub (x,p,S)),q)) by QC_LANG3:def 2

.= S_Bound (@ Z) by A7, SUBSTUT1:def 36 ;

hence S_Bound (@ Z) = S_Bound (@ Z2) ; :: thesis: verum

end;then S_Bound (@ Z2) = x. (upVar ((RestrictSub (x2,p2,S2)),q2)) by SUBSTUT1:def 36

.= [4,(upVar ((RestrictSub (x2,p2,S2)),q2))] by QC_LANG3:def 2

.= [4,(upVar ((RestrictSub (x,p,S)),q))] by A5, A2, A3, A4, Th13, Th14

.= x. (upVar ((RestrictSub (x,p,S)),q)) by QC_LANG3:def 2

.= S_Bound (@ Z) by A7, SUBSTUT1:def 36 ;

hence S_Bound (@ Z) = S_Bound (@ Z2) ; :: thesis: verum