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);
per cases ( not x in rng (RestrictSub (x,p,S)) or x in rng (RestrictSub (x,p,S)) ) ;
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;
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;
end;