let Al be QC-alphabet ; :: thesis: for k being Nat

for P being QC-pred_symbol of k,Al

for ll being CQC-variable_list of k,Al

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = P ! ll & S `2 = Sub )

let k be Nat; :: thesis: for P being QC-pred_symbol of k,Al

for ll being CQC-variable_list of k,Al

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = P ! ll & S `2 = Sub )

let P be QC-pred_symbol of k,Al; :: thesis: for ll being CQC-variable_list of k,Al

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = P ! ll & S `2 = Sub )

let ll be CQC-variable_list of k,Al; :: thesis: for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = P ! ll & S `2 = Sub )

let Sub be CQC_Substitution of Al; :: thesis: ex S being Element of CQC-Sub-WFF Al st

( S `1 = P ! ll & S `2 = Sub )

P is QC-pred_symbol of (the_arity_of P),Al by QC_LANG3:1;

then k = the_arity_of P by Lm1;

then ( [(<*P*> ^ ll),Sub] in QC-Sub-WFF Al & len ll = the_arity_of P ) by CARD_1:def 7, SUBSTUT1:def 16;

then reconsider S = [(P ! ll),Sub] as Element of QC-Sub-WFF Al by QC_LANG1:def 12;

set X = { G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } ;

{ G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } = CQC-Sub-WFF Al by SUBSTUT1:def 39;

then A1: for G being Element of QC-Sub-WFF Al st G `1 is Element of CQC-WFF Al holds

G in CQC-Sub-WFF Al ;

take S ; :: thesis: ( S is Element of CQC-Sub-WFF Al & S `1 = P ! ll & S `2 = Sub )

S `1 = P ! ll ;

then reconsider S = S as Element of CQC-Sub-WFF Al by A1;

S `2 = Sub ;

hence ( S is Element of CQC-Sub-WFF Al & S `1 = P ! ll & S `2 = Sub ) ; :: thesis: verum

for P being QC-pred_symbol of k,Al

for ll being CQC-variable_list of k,Al

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = P ! ll & S `2 = Sub )

let k be Nat; :: thesis: for P being QC-pred_symbol of k,Al

for ll being CQC-variable_list of k,Al

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = P ! ll & S `2 = Sub )

let P be QC-pred_symbol of k,Al; :: thesis: for ll being CQC-variable_list of k,Al

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = P ! ll & S `2 = Sub )

let ll be CQC-variable_list of k,Al; :: thesis: for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = P ! ll & S `2 = Sub )

let Sub be CQC_Substitution of Al; :: thesis: ex S being Element of CQC-Sub-WFF Al st

( S `1 = P ! ll & S `2 = Sub )

P is QC-pred_symbol of (the_arity_of P),Al by QC_LANG3:1;

then k = the_arity_of P by Lm1;

then ( [(<*P*> ^ ll),Sub] in QC-Sub-WFF Al & len ll = the_arity_of P ) by CARD_1:def 7, SUBSTUT1:def 16;

then reconsider S = [(P ! ll),Sub] as Element of QC-Sub-WFF Al by QC_LANG1:def 12;

set X = { G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } ;

{ G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } = CQC-Sub-WFF Al by SUBSTUT1:def 39;

then A1: for G being Element of QC-Sub-WFF Al st G `1 is Element of CQC-WFF Al holds

G in CQC-Sub-WFF Al ;

take S ; :: thesis: ( S is Element of CQC-Sub-WFF Al & S `1 = P ! ll & S `2 = Sub )

S `1 = P ! ll ;

then reconsider S = S as Element of CQC-Sub-WFF Al by A1;

S `2 = Sub ;

hence ( S is Element of CQC-Sub-WFF Al & S `1 = P ! ll & S `2 = Sub ) ; :: thesis: verum