let A be QC-alphabet ; :: thesis: for p, q, p1, q1 being Element of QC-WFF A st p '&' q = p1 '&' q1 holds
( p = p1 & q = q1 )
let p, q, p1, q1 be Element of QC-WFF A; :: 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:32;
then A2: (@ p) ^ (@ q) = (@ p1) ^ (@ q1) by A1, FINSEQ_1:33;
then A3: ( len (@ p1) <= len (@ p) implies ex sq being FinSequence st @ p = (@ p1) ^ sq ) by FINSEQ_1:47;
A4: ( len (@ p) <= len (@ p1) implies ex sq being FinSequence st @ p1 = (@ p) ^ sq ) by A2, FINSEQ_1:47;
hence p = p1 by A3, QC_LANG1:13; :: thesis: q = q1
( ex sq being FinSequence st @ p1 = (@ p) ^ sq implies p1 = p ) by QC_LANG1:13;
hence q = q1 by A1, A3, A4, FINSEQ_1:33, QC_LANG1:13; :: thesis: verum