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 k 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 k st p = P ! ll
then consider k being Element of NAT , P being QC-pred_symbol of k, l being QC-variable_list of k such that
A1: p = P ! l by QC_LANG1:def 16;
A2: { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } = {} by A1, CQC_LANG:7;
{ (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } = {} by A1, CQC_LANG:7;
then reconsider l = l as CQC-variable_list of k by A2, CQC_LANG:5;
take k ; :: thesis: ex P being QC-pred_symbol of k ex ll being CQC-variable_list of k st p = P ! ll
take P ; :: thesis: ex ll being CQC-variable_list of k st p = P ! ll
take l ; :: thesis: p = P ! l
thus p = P ! l by A1; :: thesis: verum