now

let a be set ; :: thesis: ( a in CQC-Sub-WFF implies a in dom QSub )
assume a in CQC-Sub-WFF ; :: thesis: a in dom QSub
then consider p being Element of QC-WFF , Sub being CQC_Substitution such that
A1: a = [p,Sub] by SUBSTUT1:8;

A2: now

set b = {} ;
assume not p is universal ; :: thesis: a in dom QSub
then p,Sub PQSub {} by SUBSTUT1:def 14;
then [[p,Sub],{}] in QSub by SUBSTUT1:def 15;
hence a in dom QSub by A1, FUNCT_1:1; :: thesis: verum

end;

now

set b = ExpandSub ((bound_in p),(the_scope_of p),(RestrictSub ((bound_in p),p,Sub)));
assume p is universal ; :: thesis: a in dom QSub
then p,Sub PQSub ExpandSub ((bound_in p),(the_scope_of p),(RestrictSub ((bound_in p),p,Sub))) by SUBSTUT1:def 14;
then [[p,Sub],(ExpandSub ((bound_in p),(the_scope_of p),(RestrictSub ((bound_in p),p,Sub))))] in QSub by SUBSTUT1:def 15;
hence a in dom QSub by A1, FUNCT_1:1; :: thesis: verum

end;

hence a in dom QSub by A2; :: thesis: verum

end;

then CQC-Sub-WFF c= dom QSub by TARSKI:def 3;
then A3: dom (QSub | CQC-Sub-WFF) = CQC-Sub-WFF by RELAT_1:62;
rng (QSub | CQC-Sub-WFF) c= vSUB

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in rng (QSub | CQC-Sub-WFF) or b in vSUB )
assume b in rng (QSub | CQC-Sub-WFF) ; :: thesis: b in vSUB
then consider a being set such that
A4: ( a in dom (QSub | CQC-Sub-WFF) & (QSub | CQC-Sub-WFF) . a = b ) by FUNCT_1:def 3;
A5: QSub | CQC-Sub-WFF c= QSub by RELAT_1:59;
[a,b] in QSub | CQC-Sub-WFF by A4, FUNCT_1:1;
then consider p being Element of QC-WFF , Sub being CQC_Substitution, b1 being set such that
A6: [a,b] = [[p,Sub],b1] and
A7: p,Sub PQSub b1 by A5, SUBSTUT1:def 15;

A8: now

assume not p is universal ; :: thesis: b is CQC_Substitution
then b1 = {} by A7, SUBSTUT1:def 14;
then b1 is PartFunc of bound_QC-variables,bound_QC-variables by RELSET_1:12;
then b1 is CQC_Substitution by PARTFUN1:45, SUBSTUT1:def 1;
hence b is CQC_Substitution by A6, ZFMISC_1:27; :: thesis: verum

end;

now

assume p is universal ; :: thesis: b is CQC_Substitution
then b1 = ExpandSub ((bound_in p),(the_scope_of p),(RestrictSub ((bound_in p),p,Sub))) by A7, SUBSTUT1:def 14;
hence b is CQC_Substitution by A6, ZFMISC_1:27; :: thesis: verum

end;

hence b in vSUB by A8; :: thesis: verum

end;

hence QSub | CQC-Sub-WFF is Function of CQC-Sub-WFF,vSUB by A3, FUNCT_2:2; :: thesis: verum