let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in [:QC-WFF ,vSUB :] or a in dom QSub )
assume a in [:QC-WFF ,vSUB :] ; :: thesis: a in dom QSub
then consider b, c being set such that
A1: b in QC-WFF and
A2: c in vSUB and
A3: a = [b,c] by ZFMISC_1:def 2;
reconsider Sub = c as CQC_Substitution by A2;
reconsider p = b as Element of QC-WFF by A1;

A4: now

set b = {} ;
set a = [[p,Sub],{} ];
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 A3, FUNCT_1:8; :: thesis: verum

end;

now

set b = ExpandSub (bound_in p),(the_scope_of p),(RestrictSub (bound_in p),p,Sub);
set a = [[p,Sub],(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 A3, FUNCT_1:8; :: thesis: verum

end;

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