A2: now :: thesis: ( not x in rng finSub implies finSub \/ {[x,x]} is CQC_Substitution of A )

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

A3: now :: thesis: for a being object holds not a in (dom finSub) /\ (dom Z)

consider Sub being CQC_Substitution of A such that
A4: finSub = RestrictSub (x,(All (x,p)),Sub) by A1;
set X = { y where y is bound_QC-variable of A : ( 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 of A : ( y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y ) } by A4, RELAT_1:58;
given a being object 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 of A : ( 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 of A 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:9;
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 object st a in (dom (@ finSub)) /\ (dom Z) holds
(@ finSub) . a = Z . a by A3;
then reconsider h = (@ finSub) \/ Z as Function by PARTFUN1:1;
reconsider Z = Z as Relation of (bound_QC-variables A),(bound_QC-variables A) ;
(@ finSub) \/ Z = h ;
hence finSub \/ {[x,x]} is CQC_Substitution of A by PARTFUN1:45; :: thesis: verum

end;

now :: thesis: ( x in rng finSub implies finSub \/ {[x,(x. (upVar (finSub,p)))]} is CQC_Substitution of A )

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 of A

A9: now :: thesis: for a being object holds not a in (dom finSub) /\ (dom Z)

consider Sub being CQC_Substitution of A such that
A10: finSub = RestrictSub (x,(All (x,p)),Sub) by A1;
set X = { y where y is bound_QC-variable of A : ( 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 of A : ( y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y ) } by A10, RELAT_1:58;
given a being object 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 of A : ( 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 of A 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:9;
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 object st a in (dom (@ finSub)) /\ (dom Z) holds
(@ finSub) . a = Z . a by A9;
then reconsider h = (@ finSub) \/ Z as Function by PARTFUN1:1;
reconsider Z = Z as Relation of (bound_QC-variables A),(bound_QC-variables A) ;
(@ finSub) \/ Z = h ;
hence finSub \/ {[x,(x. (upVar (finSub,p)))]} is CQC_Substitution of A by PARTFUN1:45; :: thesis: verum

end;

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