now for a being object st a in CQC-Sub-WFF Al holds
a in dom (QSub Al)let a be
object ;
( a in CQC-Sub-WFF Al implies a in dom (QSub Al) )assume
a in CQC-Sub-WFF Al
;
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;
now ( 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
;
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;
verum end; hence
a in dom (QSub Al)
by A2;
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
hence
(QSub Al) | (CQC-Sub-WFF Al) is Function of (CQC-Sub-WFF Al),(vSUB Al)
by A3, FUNCT_2:2; verum