let x1, x2 be bound_QC-variable of A; ( 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 )
; 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; verum