let q1, q2 be QC-formula; :: thesis: ( ex p being Element of QC-WFF st F = p '&' q1 & ex p being Element of QC-WFF st F = p '&' q2 implies q1 = q2 )
given p1 being Element of QC-WFF such that A2: F = p1 '&' q1 ; :: thesis: ( for p being Element of QC-WFF holds not F = p '&' q2 or q1 = q2 )
given p2 being Element of QC-WFF such that A3: F = p2 '&' q2 ; :: thesis: q1 = q2
<*[2,0]*> ^ ((@ p1) ^ (@ q1)) = p2 '&' q2 by A2, A3, FINSEQ_1:45
.= <*[2,0]*> ^ ((@ p2) ^ (@ q2)) by FINSEQ_1:45 ;
then A4: (@ p1) ^ (@ q1) = (@ p2) ^ (@ q2) by FINSEQ_1:46;
p1 = the_left_argument_of F by A1, A2, Def24
.= p2 by A1, A3, Def24 ;
hence q1 = q2 by A4, FINSEQ_1:46; :: thesis: verum