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 A1: 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 A2: F = p2 '&' q2 ; :: thesis: p1 = p2
<*[2,0]*> ^ ((@ p1) ^ (@ q1)) = p2 '&' q2 by A1, A2, FINSEQ_1:32
.= <*[2,0]*> ^ ((@ p2) ^ (@ q2)) by FINSEQ_1:32 ;
then A3: (@ 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
A4: ( ( a = @ p1 & b = @ p2 ) or ( a = @ p2 & b = @ p1 ) ) and
A5: ( len a <= len b & a ^ c = b ^ d ) by A3;
ex t being FinSequence st a ^ t = b by A5, FINSEQ_1:47;
hence p1 = p2 by A4, Th13; :: thesis: verum