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