ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st F = P ! ll by A1, Def18;
hence ex b₁ being QC-pred_symbol of A ex k being Element of NAT ex ll being QC-variable_list of k,A ex P being QC-pred_symbol of k,A st
( b₁ = P & F = P ! ll ) ; :: thesis: verum