let S1, S2 be Element of QC-Sub-WFF ; :: thesis: ( ex B being Element of [:QC-Sub-WFF ,bound_QC-variables :] ex SQ being second_Q_comp of B st
( A = Sub_All B,SQ & B `1 = S1 & B is quantifiable ) & ex B being Element of [:QC-Sub-WFF ,bound_QC-variables :] ex SQ being second_Q_comp of B st
( A = Sub_All B,SQ & B `1 = S2 & B is quantifiable ) implies S1 = S2 )
given B1 being Element of [:QC-Sub-WFF ,bound_QC-variables :], SQ1 being second_Q_comp of B1 such that A3: A = Sub_All B1,SQ1 and
A4: B1 `1 = S1 and
A5: B1 is quantifiable ; :: thesis: ( for B being Element of [:QC-Sub-WFF ,bound_QC-variables :]
for SQ being second_Q_comp of B holds
( not A = Sub_All B,SQ or not B `1 = S2 or not B is quantifiable ) or S1 = S2 )
A6: A = [(All (B1 `2 ),((B1 `1 ) `1 )),SQ1] by A3, A5, Def24;
A7: (B1 `1 ) `2 = QSub . [(All (B1 `2 ),((B1 `1 ) `1 )),SQ1] by A5, Def23;
given B2 being Element of [:QC-Sub-WFF ,bound_QC-variables :], SQ2 being second_Q_comp of B2 such that A8: A = Sub_All B2,SQ2 and
A9: B2 `1 = S2 and
A10: B2 is quantifiable ; :: thesis: S1 = S2
A11: ( B1 `1 = [((B1 `1 ) `1 ),((B1 `1 ) `2 )] & B2 `1 = [((B2 `1 ) `1 ),((B2 `1 ) `2 )] ) by Th10;
A12: A = [(All (B2 `2 ),((B2 `1 ) `1 )),SQ2] by A8, A10, Def24;
then All (B1 `2 ),((B1 `1 ) `1 ) = All (B2 `2 ),((B2 `1 ) `1 ) by A6, ZFMISC_1:33;
then (B1 `1 ) `1 = (B2 `1 ) `1 by QC_LANG2:6;
hence S1 = S2 by A4, A9, A10, A6, A12, A7, A11, Def23; :: thesis: verum