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

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