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