let Al be QC-alphabet ; :: thesis: [:(QC-WFF Al),(vSUB Al):] c= dom (QSub Al)
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in [:(QC-WFF Al),(vSUB Al):] or a in dom (QSub Al) )
assume a in [:(QC-WFF Al),(vSUB Al):] ; :: thesis: a in dom (QSub Al)
then consider b, c being object such that
A1: b in QC-WFF Al and
A2: c in vSUB Al and
A3: a = [b,c] by ZFMISC_1:def 2;
reconsider Sub = c as CQC_Substitution of Al by A2;
reconsider p = b as Element of QC-WFF Al by A1;
A4: now :: thesis: ( not p is universal implies a in dom (QSub Al) )
set b = {} ;
set a = [[p,Sub],{}];
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 A3, 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)));
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 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 A3, FUNCT_1:1; :: thesis: verum
end;
hence a in dom (QSub Al) by A4; :: thesis: verum