now :: thesis: for a being object st a in CQC-Sub-WFF Al holds

a in dom (QSub Al)

then
CQC-Sub-WFF Al c= dom (QSub Al)
;a in dom (QSub Al)

let a be object ; :: thesis: ( a in CQC-Sub-WFF Al implies a in dom (QSub Al) )

assume a in CQC-Sub-WFF Al ; :: thesis: 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;

end;assume a in CQC-Sub-WFF Al ; :: thesis: 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;

A2: now :: thesis: ( not p is universal implies a in dom (QSub Al) )

set b = {} ;

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

end;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 A1, FUNCT_1:1; :: thesis: verum

now :: thesis: ( p is universal implies a in dom (QSub Al) )

hence
a in dom (QSub Al)
by A2; :: thesis: verumset b = 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 A1, FUNCT_1:1; :: thesis: verum

end;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 A1, FUNCT_1:1; :: thesis: verum

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

proof

hence
(QSub Al) | (CQC-Sub-WFF Al) is Function of (CQC-Sub-WFF Al),(vSUB Al)
by A3, FUNCT_2:2; :: thesis: verum
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in rng ((QSub Al) | (CQC-Sub-WFF Al)) or b in vSUB Al )

assume b in rng ((QSub Al) | (CQC-Sub-WFF Al)) ; :: thesis: b in vSUB Al

then consider a being object such that

A4: ( a in dom ((QSub Al) | (CQC-Sub-WFF Al)) & ((QSub Al) | (CQC-Sub-WFF Al)) . a = b ) by FUNCT_1:def 3;

A5: (QSub Al) | (CQC-Sub-WFF Al) c= QSub Al by RELAT_1:59;

[a,b] in (QSub Al) | (CQC-Sub-WFF Al) by A4, FUNCT_1:1;

then consider p being Element of QC-WFF Al, Sub being CQC_Substitution of Al, b1 being object such that

A6: [a,b] = [[p,Sub],b1] and

A7: p,Sub PQSub b1 by A5, SUBSTUT1:def 15;

end;assume b in rng ((QSub Al) | (CQC-Sub-WFF Al)) ; :: thesis: b in vSUB Al

then consider a being object such that

A4: ( a in dom ((QSub Al) | (CQC-Sub-WFF Al)) & ((QSub Al) | (CQC-Sub-WFF Al)) . a = b ) by FUNCT_1:def 3;

A5: (QSub Al) | (CQC-Sub-WFF Al) c= QSub Al by RELAT_1:59;

[a,b] in (QSub Al) | (CQC-Sub-WFF Al) by A4, FUNCT_1:1;

then consider p being Element of QC-WFF Al, Sub being CQC_Substitution of Al, b1 being object such that

A6: [a,b] = [[p,Sub],b1] and

A7: p,Sub PQSub b1 by A5, SUBSTUT1:def 15;

A8: now :: thesis: ( not p is universal implies b is CQC_Substitution of Al )

A9:
( b1 is CQC_Substitution of Al iff b1 is Element of PFuncs ((bound_QC-variables Al),(bound_QC-variables Al)) )
by SUBSTUT1:def 1;

assume not p is universal ; :: thesis: b is CQC_Substitution of Al

then b1 = {} by A7, SUBSTUT1:def 14;

then b1 is PartFunc of (bound_QC-variables Al),(bound_QC-variables Al) by RELSET_1:12;

hence b is CQC_Substitution of Al by A9, A6, PARTFUN1:45, XTUPLE_0:1; :: thesis: verum

end;assume not p is universal ; :: thesis: b is CQC_Substitution of Al

then b1 = {} by A7, SUBSTUT1:def 14;

then b1 is PartFunc of (bound_QC-variables Al),(bound_QC-variables Al) by RELSET_1:12;

hence b is CQC_Substitution of Al by A9, A6, PARTFUN1:45, XTUPLE_0:1; :: thesis: verum

now :: thesis: ( p is universal implies b is CQC_Substitution of Al )

hence
b in vSUB Al
by A8; :: thesis: verumassume
p is universal
; :: thesis: b is CQC_Substitution of Al

then b1 = ExpandSub ((bound_in p),(the_scope_of p),(RestrictSub ((bound_in p),p,Sub))) by A7, SUBSTUT1:def 14;

hence b is CQC_Substitution of Al by A6, XTUPLE_0:1; :: thesis: verum

end;then b1 = ExpandSub ((bound_in p),(the_scope_of p),(RestrictSub ((bound_in p),p,Sub))) by A7, SUBSTUT1:def 14;

hence b is CQC_Substitution of Al by A6, XTUPLE_0:1; :: thesis: verum