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