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:8; :: 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:8; :: 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:91;
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 5;
A5: QSub | CQC-Sub-WFF c= QSub by RELAT_1:88;
[a,b] in QSub | CQC-Sub-WFF by A4, FUNCT_1:8;
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:25;
then b1 is CQC_Substitution by PARTFUN1:119, SUBSTUT1:def 1;
hence b is CQC_Substitution by A6, ZFMISC_1:33; :: 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:33; :: 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:4; :: thesis: verum