now :: thesis: for a being object st a in CQC-Sub-WFF Al holds
a in dom (QSub Al)

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

A2: now :: thesis: ( not p is universal implies a in dom (QSub Al) )

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

end;

now :: thesis: ( p is universal implies a in dom (QSub Al) )

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 Al)
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 Al by SUBSTUT1:def 15;
hence a in dom (QSub Al) by A1, FUNCT_1:1; :: thesis: verum

end;

hence a in dom (QSub Al) by A2; :: thesis: verum

end;

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

proof

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

A8: now :: thesis: ( not p is universal implies b is CQC_Substitution of Al )

A9: ( b1 is CQC_Substitution of Al iff b1 is Element of PFuncs ((bound_QC-variables Al),(bound_QC-variables Al)) ) by SUBSTUT1:def 1;
assume not p is universal ; :: thesis: b is CQC_Substitution of Al
then b1 = {} by A7, SUBSTUT1:def 14;
then b1 is PartFunc of (bound_QC-variables Al),(bound_QC-variables Al) by RELSET_1:12;
hence b is CQC_Substitution of Al by A9, A6, PARTFUN1:45, XTUPLE_0:1; :: thesis: verum

end;

now :: thesis: ( p is universal implies b is CQC_Substitution of Al )

assume p is universal ; :: thesis: b is CQC_Substitution of Al
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 of Al by A6, XTUPLE_0:1; :: thesis: verum

end;

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

end;

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