:: deftheorem defines ExpandSub SUBSTUT1:def 13 :
for A being QC-alphabet
for x being bound_QC-variable of A
for p being QC-formula of A
for finSub being finite CQC_Substitution of A st ex Sub being CQC_Substitution of A st finSub = RestrictSub (x,(All (x,p)),Sub) holds
( ( x in rng finSub implies ExpandSub (x,p,finSub) = finSub \/ {[x,(x. (upVar (finSub,p)))]} ) & ( not x in rng finSub implies ExpandSub (x,p,finSub) = finSub \/ {[x,x]} ) );