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:27;
then (B1 `1) `1 = (B2 `1) `1 by QC_LANG2:5;
hence S1 = S2 by A4, A9, A10, A6, A12, A7, A11, Def23; :: thesis: verum