let q1, q2 be QC-formula of A; ( ex p being Element of QC-WFF A st F = p '&' q1 & ex p being Element of QC-WFF A st F = p '&' q2 implies q1 = q2 )
given p1 being Element of QC-WFF A such that A2:
F = p1 '&' q1
; ( for p being Element of QC-WFF A holds not F = p '&' q2 or q1 = q2 )
given p2 being Element of QC-WFF A such that A3:
F = p2 '&' q2
; q1 = q2
<*[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;
p1 =
the_left_argument_of F
by A1, A2, Def25
.=
p2
by A1, A3, Def25
;
hence
q1 = q2
by A4, FINSEQ_1:33; verum