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

proof

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

end;

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