let p be Element of CQC-WFF ; :: thesis: ( p is atomic implies ex k being Element of NAT ex P being QC-pred_symbol of k ex ll being CQC-variable_list of st p = P ! ll )
assume p is atomic ; :: thesis: ex k being Element of NAT ex P being QC-pred_symbol of k ex ll being CQC-variable_list of st p = P ! ll
then consider k being Element of NAT , P being QC-pred_symbol of k, ll being QC-variable_list of such that
A1: p = P ! ll by QC_LANG1:def 17;
( { (ll . i) where i is Element of NAT : ( 1 <= i & i <= len ll & ll . i in free_QC-variables ) } = {} & { (ll . m) where m is Element of NAT : ( 1 <= m & m <= len ll & ll . m in fixed_QC-variables ) } = {} ) by A1, CQC_LANG:17;
then ll is CQC-variable_list of by CQC_LANG:15;
hence ex k being Element of NAT ex P being QC-pred_symbol of k ex ll being CQC-variable_list of st p = P ! ll by A1; :: thesis: verum