let x1, x2 be bound_QC-variable; :: thesis: ( ( for p being Element of CQC-WFF st p = F . a holds
x1 = Ex-bound_in p ) & ( for p being Element of CQC-WFF st p = F . a holds
x2 = Ex-bound_in p ) implies x1 = x2 )
assume that
A1: for p being Element of CQC-WFF st p = F . a holds
x1 = Ex-bound_in p and
A2: for p being Element of CQC-WFF st p = F . a holds
x2 = Ex-bound_in p ; :: thesis: x1 = x2
reconsider q = F . a as Element of CQC-WFF ;
x1 = Ex-bound_in q by A1;
hence x1 = x2 by A2; :: thesis: verum