A1: dom (QSub | CQC-Sub-WFF ) = CQC-Sub-WFF

proof

now

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

A4: now

assume A5: p is universal ; :: thesis: a in dom QSub
set b = ExpandSub (bound_in p),(the_scope_of p),(RestrictSub (bound_in p),p,Sub);
p,Sub PQSub ExpandSub (bound_in p),(the_scope_of p),(RestrictSub (bound_in p),p,Sub) by A5, 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 A3, FUNCT_1:8; :: thesis: verum

end;

now

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

end;

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

end;

then CQC-Sub-WFF c= dom QSub by TARSKI:def 3;
hence dom (QSub | CQC-Sub-WFF ) = CQC-Sub-WFF by RELAT_1:91; :: thesis: verum

end;

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 A7: b in rng (QSub | CQC-Sub-WFF ) ; :: thesis: b in vSUB
consider a being set such that
A8: ( a in dom (QSub | CQC-Sub-WFF ) & (QSub | CQC-Sub-WFF ) . a = b ) by A7, FUNCT_1:def 5;
A9: [a,b] in QSub | CQC-Sub-WFF by A8, FUNCT_1:8;
QSub | CQC-Sub-WFF c= QSub by RELAT_1:88;
then consider p being Element of QC-WFF , Sub being CQC_Substitution, b1 being set such that
A10: ( [a,b] = [[p,Sub],b1] & p,Sub PQSub b1 ) by A9, SUBSTUT1:def 15;

A11: 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 A10, SUBSTUT1:def 14;
hence b is CQC_Substitution by A10, ZFMISC_1:33; :: thesis: verum

end;

now

assume not p is universal ; :: thesis: b is CQC_Substitution
then b1 = {} by A10, 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 A10, ZFMISC_1:33; :: thesis: verum

end;

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

end;

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