let x1, x2 be bound_QC-variable of A; :: thesis: ( ex p being Element of QC-WFF A st F = All (x1,p) & ex p being Element of QC-WFF A st F = All (x2,p) implies x1 = x2 )
given p1 being Element of QC-WFF A such that A2: F = All (x1,p1) ; :: thesis: ( for p being Element of QC-WFF A holds not F = All (x2,p) or x1 = x2 )
given p2 being Element of QC-WFF A such that A3: F = All (x2,p2) ; :: thesis: x1 = x2
<*[3,0]*> ^ (<*x1*> ^ (@ p1)) = All (x2,p2) by A2, A3, FINSEQ_1:32
.= <*[3,0]*> ^ (<*x2*> ^ (@ p2)) by FINSEQ_1:32 ;
then A4: <*x1*> ^ (@ p1) = <*x2*> ^ (@ p2) by FINSEQ_1:33;
thus x1 = (<*x1*> ^ (@ p1)) . 1 by FINSEQ_1:41
.= x2 by A4, FINSEQ_1:41 ; :: thesis: verum