let F, G be Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)); ( ( 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) ) & ( 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
G . (t,h) = All ((x. t),p) ) implies F = G )
assume A3:
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)
; ( ex t being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) ex p being Element of CQC-WFF A st
( p = f . ((t ++),(h +* (x .--> (x. t)))) & not G . (t,h) = All ((x. t),p) ) or F = G )
assume A4:
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
G . (t,h) = All ((x. t),p)
; F = G
for a being Element of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] holds F . a = G . a
proof
let a be
Element of
[:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):];
F . a = G . a
consider k being
Element of
QC-symbols A,
h being
Element of
Funcs (
(bound_QC-variables A),
(bound_QC-variables A))
such that A5:
a = [k,h]
by DOMAIN_1:1;
reconsider h2 =
h +* (x .--> (x. k)) 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 p =
f . (
(k ++),
h2) as
Element of
CQC-WFF A ;
F . (
k,
h) =
All (
(x. k),
p)
by A3
.=
G . (
k,
h)
by A4
;
hence
F . a = G . a
by A5;
verum
end;
hence
F = G
by FUNCT_2:63; verum