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:1; :: 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:1; :: thesis: verum

end;

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