let p1, p2 be QC-formula of A; ( 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
; ( 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
; 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; verum