let p1, p2 be QC-formula of A; :: thesis: ( ex q being Element of QC-WFF A st F = p1 '&' q & ex q being Element of QC-WFF A st F = p2 '&' q implies p1 = p2 )
given q1 being Element of QC-WFF A such that A2: F = p1 '&' q1 ; :: thesis: ( for q being Element of QC-WFF A holds not F = p2 '&' q or p1 = p2 )
given q2 being Element of QC-WFF A such that A3: F = p2 '&' q2 ; :: thesis: p1 = p2
<*[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;
( len (@ p1) <= len (@ p2) or len (@ p2) <= len (@ p1) ) ;
then consider a, b, c, d being FinSequence such that
A5: ( ( a = @ p1 & b = @ p2 ) or ( a = @ p2 & b = @ p1 ) ) and
A6: ( len a <= len b & a ^ c = b ^ d ) by A4;
ex t being FinSequence st a ^ t = b by A6, FINSEQ_1:47;
hence p1 = p2 by A5, Th13; :: thesis: verum