let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al st ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st
( S `1 = p & S `2 = Sub ) ) holds
for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st
( S `1 = All (x,p) & S `2 = Sub )
let p be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al st ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st
( S `1 = p & S `2 = Sub ) ) holds
for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st
( S `1 = All (x,p) & S `2 = Sub )
let x be bound_QC-variable of Al; :: thesis: ( ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st
( S `1 = p & S `2 = Sub ) ) implies for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st
( S `1 = All (x,p) & S `2 = Sub ) )
assume A1: for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st
( S `1 = p & S `2 = Sub ) ; :: thesis: for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st
( S `1 = All (x,p) & S `2 = Sub )
let Sub be CQC_Substitution of Al; :: thesis: ex S being Element of CQC-Sub-WFF Al st
( S `1 = All (x,p) & S `2 = Sub )
set Sub1 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub]));
( (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) is CQC_Substitution of Al iff (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) is Element of PFuncs ((bound_QC-variables Al),(bound_QC-variables Al)) ) by SUBSTUT1:def 1;
then reconsider Sub1 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) as CQC_Substitution of Al by PARTFUN1:45;
ex S being Element of CQC-Sub-WFF Al st
( S `1 = p & S `2 = Sub1 ) by A1;
then consider S1 being Element of CQC-Sub-WFF Al such that
A2: S1 = [(All (x,p)),Sub] by Th10;
take S1 ; :: thesis: ( S1 `1 = All (x,p) & S1 `2 = Sub )
thus ( S1 `1 = All (x,p) & S1 `2 = Sub ) by A2; :: thesis: verum