let S1, S2 be Element of QC-Sub-WFF A; :: thesis: ( ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( A2 = Sub_All (B,SQ) & B `1 = S1 & B is quantifiable ) & ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( A2 = Sub_All (B,SQ) & B `1 = S2 & B is quantifiable ) implies S1 = S2 )
given B1 being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ1 being second_Q_comp of B1 such that A3: A2 = Sub_All (B1,SQ1) and
A4: B1 `1 = S1 and
A5: B1 is quantifiable ; :: thesis: ( for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]
for SQ being second_Q_comp of B holds
( not A2 = Sub_All (B,SQ) or not B `1 = S2 or not B is quantifiable ) or S1 = S2 )
A6: A2 = [(All ((B1 `2),((B1 `1) `1))),SQ1] by A3, A5, Def24;
A7: (B1 `1) `2 = (QSub A) . [(All ((B1 `2),((B1 `1) `1))),SQ1] by A5, Def23;
given B2 being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ2 being second_Q_comp of B2 such that A8: A2 = 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: A2 = [(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, XTUPLE_0:1;
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