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