defpred S1[ 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 S1[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 S1[k,h,u]let h be
Element of
Funcs bound_QC-variables ,
bound_QC-variables ;
:: thesis: ex u being Element of CQC-WFF st S1[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: S1[k,h, All (x. k),q]
thus
S1[
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 S1[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