let p, q, p1, q1 be Element of QC-WFF ; :: thesis: ( p '&' q = p1 '&' q1 implies ( p = p1 & q = q1 ) )
assume A1: p '&' q = p1 '&' q1 ; :: thesis: ( p = p1 & q = q1 )
( (<*[2,0]*> ^ (@ p)) ^ (@ q) = <*[2,0]*> ^ ((@ p) ^ (@ q)) & (<*[2,0]*> ^ (@ p1)) ^ (@ q1) = <*[2,0]*> ^ ((@ p1) ^ (@ q1)) ) by FINSEQ_1:45;
then A2: (@ p) ^ (@ q) = (@ p1) ^ (@ q1) by A1, FINSEQ_1:46;
then A3: ( len (@ p1) <= len (@ p) implies ex sq being FinSequence st @ p = (@ p1) ^ sq ) by FINSEQ_1:64;
A4: ( len (@ p) <= len (@ p1) implies ex sq being FinSequence st @ p1 = (@ p) ^ sq ) by A2, FINSEQ_1:64;
hence p = p1 by A3, QC_LANG1:37; :: thesis: q = q1
( ex sq being FinSequence st @ p1 = (@ p) ^ sq implies p1 = p ) by QC_LANG1:37;
hence q = q1 by A1, A3, A4, FINSEQ_1:46, QC_LANG1:37; :: thesis: verum