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 A2: A2 = Sub_All (B1,SQ1) and
A3: B1 `1 = S1 and
A4: 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 )
A5: A2 = [(All ((B1 `2),((B1 `1) `1))),SQ1] by A2, A4, Def24;
A6: (B1 `1) `2 = (QSub A) . [(All ((B1 `2),((B1 `1) `1))),SQ1] by A4, Def23;
given B2 being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ2 being second_Q_comp of B2 such that A7: A2 = Sub_All (B2,SQ2) and
A8: B2 `1 = S2 and
A9: B2 is quantifiable ; :: thesis: S1 = S2
A10: ( B1 `1 = [((B1 `1) `1),((B1 `1) `2)] & B2 `1 = [((B2 `1) `1),((B2 `1) `2)] ) by Th10;
A11: A2 = [(All ((B2 `2),((B2 `1) `1))),SQ2] by A7, A9, Def24;
then All ((B1 `2),((B1 `1) `1)) = All ((B2 `2),((B2 `1) `1)) by A5, XTUPLE_0:1;
then (B1 `1) `1 = (B2 `1) `1 by QC_LANG2:5;
hence S1 = S2 by A3, A8, A9, A5, A11, A6, A10, Def23; :: thesis: verum