set Al2 = FCEx Al;

[:NAT,(QC-symbols (FCEx Al)):] = [:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[y,q]] where q is Element of CQC-WFF Al, y is bound_QC-variable of Al : verum } ):] by QC_LANG1:5;

then A1: QC-symbols (FCEx Al) = (QC-symbols Al) \/ { [ the free_symbol of Al,[y,q]] where q is Element of CQC-WFF Al, y is bound_QC-variable of Al : verum } by ZFMISC_1:110;

[ the free_symbol of Al,[x,p]] in { [ the free_symbol of Al,[y,q]] where q is Element of CQC-WFF Al, y is bound_QC-variable of Al : verum } ;

then A2: [ the free_symbol of Al,[x,p]] in QC-symbols (FCEx Al) by A1, XBOOLE_0:def 3;

4 in {4} by TARSKI:def 1;

then [4,[ the free_symbol of Al,[x,p]]] in [:{4},(QC-symbols (FCEx Al)):] by A2, ZFMISC_1:87;

hence [4,[ the free_symbol of Al,[x,p]]] is bound_QC-variable of (FCEx Al) by QC_LANG1:def 4; :: thesis: verum

[:NAT,(QC-symbols (FCEx Al)):] = [:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[y,q]] where q is Element of CQC-WFF Al, y is bound_QC-variable of Al : verum } ):] by QC_LANG1:5;

then A1: QC-symbols (FCEx Al) = (QC-symbols Al) \/ { [ the free_symbol of Al,[y,q]] where q is Element of CQC-WFF Al, y is bound_QC-variable of Al : verum } by ZFMISC_1:110;

[ the free_symbol of Al,[x,p]] in { [ the free_symbol of Al,[y,q]] where q is Element of CQC-WFF Al, y is bound_QC-variable of Al : verum } ;

then A2: [ the free_symbol of Al,[x,p]] in QC-symbols (FCEx Al) by A1, XBOOLE_0:def 3;

4 in {4} by TARSKI:def 1;

then [4,[ the free_symbol of Al,[x,p]]] in [:{4},(QC-symbols (FCEx Al)):] by A2, ZFMISC_1:87;

hence [4,[ the free_symbol of Al,[x,p]]] is bound_QC-variable of (FCEx Al) by QC_LANG1:def 4; :: thesis: verum