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:8;
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