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

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

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

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

then consider k being Nat, P being QC-pred_symbol of k,Al, l being QC-variable_list of k,Al such that

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

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

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

then reconsider l = l as CQC-variable_list of k,Al by A2, CQC_LANG:5;

take k ; :: thesis: ex P being QC-pred_symbol of k,Al ex ll being CQC-variable_list of k,Al st p = P ! ll

take P ; :: thesis: ex ll being CQC-variable_list of k,Al st p = P ! ll

take l ; :: thesis: p = P ! l

thus p = P ! l by A1; :: thesis: verum

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

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

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

then consider k being Nat, P being QC-pred_symbol of k,Al, l being QC-variable_list of k,Al such that

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

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

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

then reconsider l = l as CQC-variable_list of k,Al by A2, CQC_LANG:5;

take k ; :: thesis: ex P being QC-pred_symbol of k,Al ex ll being CQC-variable_list of k,Al st p = P ! ll

take P ; :: thesis: ex ll being CQC-variable_list of k,Al st p = P ! ll

take l ; :: thesis: p = P ! l

thus p = P ! l by A1; :: thesis: verum