let F, G be Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)); :: thesis: ( ( 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) ; :: thesis: ( 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) ; :: thesis: 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))):]; :: thesis: 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; :: thesis: verum

end;

hence F = G by FUNCT_2:63; :: thesis: verum