let p1, p2 be QC-formula of A; :: thesis: ( ex x being bound_QC-variable of A st F = All (x,p1) & ex x being bound_QC-variable of A st F = All (x,p2) implies p1 = p2 )
given x1 being bound_QC-variable of A such that A5: F = All (x1,p1) ; :: thesis: ( for x being bound_QC-variable of A holds not F = All (x,p2) or p1 = p2 )
given x2 being bound_QC-variable of A such that A6: F = All (x2,p2) ; :: thesis: p1 = p2
<*[3,0]*> ^ (<*x1*> ^ (@ p1)) = All (x2,p2) by A5, A6, FINSEQ_1:32
.= <*[3,0]*> ^ (<*x2*> ^ (@ p2)) by FINSEQ_1:32 ;
then A7: <*x1*> ^ (@ p1) = <*x2*> ^ (@ p2) by FINSEQ_1:33;
x1 = (<*x1*> ^ (@ p1)) . 1 by FINSEQ_1:41
.= x2 by A7, FINSEQ_1:41 ;
hence p1 = p2 by A7, FINSEQ_1:33; :: thesis: verum