defpred S₁[ Element of QC-symbols A, Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)), set ] means for p being Element of CQC-WFF A st p = f . [($1 ++),($2 +* ({x} --> (x. $1)))] holds
$3 = All ((x. $1),p);
A1: for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) ex u being Element of CQC-WFF A st S₁[t,h,u]

proof

let t be QC-symbol of A; :: thesis: for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) ex u being Element of CQC-WFF A st S₁[t,h,u]
let h be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: ex u being Element of CQC-WFF A st S₁[t,h,u]
reconsider h2 = h +* (x .--> (x. t)) as Function of (bound_QC-variables A),(bound_QC-variables A) by Lm1;
reconsider h2 = h2 as Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) by FUNCT_2:8;
reconsider q = f . [(t ++),h2] as Element of CQC-WFF A ;
take All ((x. t),q) ; :: thesis: S₁[t,h, All ((x. t),q)]
thus S₁[t,h, All ((x. t),q)] ; :: thesis: verum

end;

consider F being Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A) such that
A2: for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds S₁[t,h,F . (t,h)] from BINOP_1:sch 3(A1);
reconsider F = F as Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) by FUNCT_2:8;
take F ; :: thesis: for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for p being Element of CQC-WFF A st p = f . ((t ++),(h +* (x .--> (x. t)))) holds
F . (t,h) = All ((x. t),p)
let t be QC-symbol of A; :: thesis: for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for p being Element of CQC-WFF A st p = f . ((t ++),(h +* (x .--> (x. t)))) holds
F . (t,h) = All ((x. t),p)
let h be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: for p being Element of CQC-WFF A st p = f . ((t ++),(h +* (x .--> (x. t)))) holds
F . (t,h) = All ((x. t),p)
let p be Element of CQC-WFF A; :: thesis: ( p = f . ((t ++),(h +* (x .--> (x. t)))) implies F . (t,h) = All ((x. t),p) )
assume p = f . ((t ++),(h +* (x .--> (x. t)))) ; :: thesis: F . (t,h) = All ((x. t),p)
hence F . (t,h) = All ((x. t),p) by A2; :: thesis: verum