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 )
( p '&' q = (<*[2,0 ]*> ^ (@ p)) ^ (@ q) & p1 '&' q1 = (<*[2,0 ]*> ^ (@ p1)) ^ (@ q1) & (<*[2,0 ]*> ^ (@ p)) ^ (@ q) = <*[2,0 ]*> ^ ((@ p) ^ (@ q)) & (<*[2,0 ]*> ^ (@ p1)) ^ (@ q1) = <*[2,0 ]*> ^ ((@ p1) ^ (@ q1)) ) by FINSEQ_1:45;
then (@ p) ^ (@ q) = (@ p1) ^ (@ q1) by A1, FINSEQ_1:46;
then A2: ( ( len (@ p) <= len (@ p1) or len (@ p1) <= len (@ p) ) & ( len (@ p1) <= len (@ p) implies ex sq being FinSequence st @ p = (@ p1) ^ sq ) & ( len (@ p) <= len (@ p1) implies ex sq being FinSequence st @ p1 = (@ p) ^ sq ) ) by FINSEQ_1:64;
A3: ( ex sq being FinSequence st @ p1 = (@ p) ^ sq implies p1 = p ) by QC_LANG1:37;
thus p = p1 by A2, QC_LANG1:37; :: thesis: q = q1
thus q = q1 by A1, A2, A3, FINSEQ_1:46, QC_LANG1:37; :: thesis: verum