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