A2: now

reconsider Z = {[x,x]} as Relation-like set ;
assume not x in rng finSub ; :: thesis: finSub \/ {[x,x]} is CQC_Substitution

A3: now

consider Sub being CQC_Substitution such that
A4: finSub = RestrictSub x,(All x,p),Sub by A1;
set X = { y where y is bound_QC-variable : ( y in still_not-bound_in (All x,p) & y is Element of dom Sub & y <> x & y <> Sub . y ) } ;
A5: dom finSub c= { y where y is bound_QC-variable : ( y in still_not-bound_in (All x,p) & y is Element of dom Sub & y <> x & y <> Sub . y ) } by A4, RELAT_1:87;
given a being set such that A6: a in (dom finSub) /\ (dom Z) ; :: thesis: contradiction
a in dom finSub by A6, XBOOLE_0:def 4;
then a in { y where y is bound_QC-variable : ( y in still_not-bound_in (All x,p) & y is Element of dom Sub & y <> x & y <> Sub . y ) } by A5;
then A7: ( dom Z = {x} & ex y being bound_QC-variable st
( a = y & y in still_not-bound_in (All x,p) & y is Element of dom Sub & y <> x & y <> Sub . y ) ) by RELAT_1:23;
a in dom Z by A6, XBOOLE_0:def 4;
hence contradiction by A7, TARSKI:def 1; :: thesis: verum

end;

reconsider Z = Z as Function ;
for a being set st a in (dom (@ finSub)) /\ (dom Z) holds
(@ finSub) . a = Z . a by A3;
then consider h being Function such that
A8: (@ finSub) \/ Z = h by PARTFUN1:2;
reconsider Z = Z as Relation of bound_QC-variables ,bound_QC-variables ;
(@ finSub) \/ Z = h by A8;
hence finSub \/ {[x,x]} is CQC_Substitution by PARTFUN1:119; :: thesis: verum

end;

now

reconsider Z = {[x,(x. (upVar finSub,p))]} as Relation-like set ;
assume x in rng finSub ; :: thesis: finSub \/ {[x,(x. (upVar finSub,p))]} is CQC_Substitution

A9: now

consider Sub being CQC_Substitution such that
A10: finSub = RestrictSub x,(All x,p),Sub by A1;
set X = { y where y is bound_QC-variable : ( y in still_not-bound_in (All x,p) & y is Element of dom Sub & y <> x & y <> Sub . y ) } ;
A11: dom finSub c= { y where y is bound_QC-variable : ( y in still_not-bound_in (All x,p) & y is Element of dom Sub & y <> x & y <> Sub . y ) } by A10, RELAT_1:87;
given a being set such that A12: a in (dom finSub) /\ (dom Z) ; :: thesis: contradiction
a in dom finSub by A12, XBOOLE_0:def 4;
then a in { y where y is bound_QC-variable : ( y in still_not-bound_in (All x,p) & y is Element of dom Sub & y <> x & y <> Sub . y ) } by A11;
then A13: ( dom Z = {x} & ex y being bound_QC-variable st
( a = y & y in still_not-bound_in (All x,p) & y is Element of dom Sub & y <> x & y <> Sub . y ) ) by RELAT_1:23;
a in dom Z by A12, XBOOLE_0:def 4;
hence contradiction by A13, TARSKI:def 1; :: thesis: verum

end;

reconsider Z = Z as Function ;
for a being set st a in (dom (@ finSub)) /\ (dom Z) holds
(@ finSub) . a = Z . a by A9;
then consider h being Function such that
A14: (@ finSub) \/ Z = h by PARTFUN1:2;
reconsider Z = Z as Relation of bound_QC-variables ,bound_QC-variables ;
(@ finSub) \/ Z = h by A14;
hence finSub \/ {[x,(x. (upVar finSub,p))]} is CQC_Substitution by PARTFUN1:119; :: thesis: verum

end;

hence ( ( x in rng finSub implies finSub \/ {[x,(x. (upVar finSub,p))]} is CQC_Substitution ) & ( not x in rng finSub implies finSub \/ {[x,x]} is CQC_Substitution ) ) by A2; :: thesis: verum