deffunc H₁( set , Element of Funcs bound_QC-variables ,bound_QC-variables ) -> Element of CQC-WFF = P ! ($2 * l);
consider f being Function of [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF such that
A1: for n being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables holds f . n,h = H₁(n,h) from BINOP_1:sch 4();
f is Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF by FUNCT_2:11;
hence ex b₁ being Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF st
for n being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables holds b₁ . n,h = P ! (h * l) by A1; :: thesis: verum