let x1, x2 be bound_QC-variable of A; :: thesis: ( ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( S = Sub_All (B,SQ) & B `2 = x1 & 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
( S = Sub_All (B,SQ) & B `2 = x2 & B is quantifiable ) implies x1 = x2 )
assume that
A3: ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( S = Sub_All (B,SQ) & B `2 = x1 & B is quantifiable ) and
A4: ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( S = Sub_All (B,SQ) & B `2 = x2 & B is quantifiable ) ; :: thesis: x1 = x2
consider B1 being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ1 being second_Q_comp of B1 such that
A5: S = Sub_All (B1,SQ1) and
A6: B1 `2 = x1 and
A7: B1 is quantifiable by A3;
consider B2 being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ2 being second_Q_comp of B2 such that
A8: S = Sub_All (B2,SQ2) and
A9: B2 `2 = x2 and
A10: B2 is quantifiable by A4;
A11: [(All ((B2 `2),((B2 `1) `1))),SQ2] = S by A8, A10, Def24;
[(All ((B1 `2),((B1 `1) `1))),SQ1] = S by A5, A7, Def24;
then All ((B1 `2),((B1 `1) `1)) = All ((B2 `2),((B2 `1) `1)) by A11, XTUPLE_0:1;
hence x1 = x2 by A6, A9, QC_LANG2:5; :: thesis: verum