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