let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A st p is atomic holds

ex k being Nat ex P being QC-pred_symbol of k,A ex ll being CQC-variable_list of k,A st p = P ! ll

let p be Element of CQC-WFF A; :: thesis: ( p is atomic implies ex k being Nat ex P being QC-pred_symbol of k,A ex ll being CQC-variable_list of k,A st p = P ! ll )

assume p is atomic ; :: thesis: ex k being Nat ex P being QC-pred_symbol of k,A ex ll being CQC-variable_list of k,A st p = P ! ll

then consider k being Nat, P being QC-pred_symbol of k,A, ll being QC-variable_list of k,A such that

A1: p = P ! ll by QC_LANG1:def 18;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

reconsider ll = ll as QC-variable_list of k,A ;

A2: { (ll . m) where m is Nat : ( 1 <= m & m <= len ll & ll . m in fixed_QC-variables A ) } = {} by A1, CQC_LANG:7;

{ (ll . i) where i is Nat : ( 1 <= i & i <= len ll & ll . i in free_QC-variables A ) } = {} by A1, CQC_LANG:7;

then ll is CQC-variable_list of k,A by A2, CQC_LANG:5;

hence ex k being Nat ex P being QC-pred_symbol of k,A ex ll being CQC-variable_list of k,A st p = P ! ll by A1; :: thesis: verum

ex k being Nat ex P being QC-pred_symbol of k,A ex ll being CQC-variable_list of k,A st p = P ! ll

let p be Element of CQC-WFF A; :: thesis: ( p is atomic implies ex k being Nat ex P being QC-pred_symbol of k,A ex ll being CQC-variable_list of k,A st p = P ! ll )

assume p is atomic ; :: thesis: ex k being Nat ex P being QC-pred_symbol of k,A ex ll being CQC-variable_list of k,A st p = P ! ll

then consider k being Nat, P being QC-pred_symbol of k,A, ll being QC-variable_list of k,A such that

A1: p = P ! ll by QC_LANG1:def 18;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

reconsider ll = ll as QC-variable_list of k,A ;

A2: { (ll . m) where m is Nat : ( 1 <= m & m <= len ll & ll . m in fixed_QC-variables A ) } = {} by A1, CQC_LANG:7;

{ (ll . i) where i is Nat : ( 1 <= i & i <= len ll & ll . i in free_QC-variables A ) } = {} by A1, CQC_LANG:7;

then ll is CQC-variable_list of k,A by A2, CQC_LANG:5;

hence ex k being Nat ex P being QC-pred_symbol of k,A ex ll being CQC-variable_list of k,A st p = P ! ll by A1; :: thesis: verum