defpred S1[ 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 S1[t,h,u]
proof
let t be
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 S1[t,h,u]let h be
Element of
Funcs (
(bound_QC-variables A),
(bound_QC-variables A));
ex u being Element of CQC-WFF A st S1[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)
;
S1[t,h, All ((x. t),q)]
thus
S1[
t,
h,
All (
(x. t),
q)]
;
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 S1[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
; 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; 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)); 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; ( p = f . ((t ++),(h +* (x .--> (x. t)))) implies F . (t,h) = All ((x. t),p) )
assume
p = f . ((t ++),(h +* (x .--> (x. t))))
; F . (t,h) = All ((x. t),p)
hence
F . (t,h) = All ((x. t),p)
by A2; verum