begin
Lm1:
for Al being QC-alphabet
for k being Element of NAT
for P being QC-pred_symbol of k,Al
for k, l being Element of NAT st P is QC-pred_symbol of k,Al & P is QC-pred_symbol of l,Al holds
k = l
theorem Th9:
for
Al being
QC-alphabet for
p being
Element of
CQC-WFF Al for
x being
bound_QC-variable of
Al for
Sub being
CQC_Substitution of
Al holds
ExpandSub (
x,
p,
(RestrictSub (x,(All (x,p)),Sub)))
= (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub]))
begin
begin