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 & c in vSUB & a = [b,c] ) by ZFMISC_1:def 2;
reconsider p = b as Element of QC-WFF by A1;
reconsider Sub = c as CQC_Substitution by A1;

A2: now

assume A3: p is universal ; :: thesis: a in dom QSub
set b = ExpandSub (bound_in p),(the_scope_of p),(RestrictSub (bound_in p),p,Sub);
A4: p,Sub PQSub ExpandSub (bound_in p),(the_scope_of p),(RestrictSub (bound_in p),p,Sub) by A3, SUBSTUT1:def 14;
set a = [[p,Sub],(ExpandSub (bound_in p),(the_scope_of p),(RestrictSub (bound_in p),p,Sub))];
[[p,Sub],(ExpandSub (bound_in p),(the_scope_of p),(RestrictSub (bound_in p),p,Sub))] in QSub by A4, SUBSTUT1:def 15;
hence a in dom QSub by A1, FUNCT_1:8; :: thesis: verum

end;

now

assume A5: not p is universal ; :: thesis: a in dom QSub
set b = {} ;
A6: p,Sub PQSub {} by A5, SUBSTUT1:def 14;
set a = [[p,Sub],{} ];
[[p,Sub],{} ] in QSub by A6, 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