let x, y be bound_QC-variable; :: thesis: for p, q being Element of QC-WFF st All x,p = All y,q holds
( x = y & p = q )
let p, q be Element of QC-WFF ; :: thesis: ( All x,p = All y,q implies ( x = y & p = q ) )
A1: ( (<*[3,0 ]*> ^ <*x*>) ^ (@ p) = <*[3,0 ]*> ^ (<*x*> ^ (@ p)) & (<*[3,0 ]*> ^ <*y*>) ^ (@ q) = <*[3,0 ]*> ^ (<*y*> ^ (@ q)) ) by FINSEQ_1:45;
A2: ( (<*x*> ^ (@ p)) . 1 = x & (<*y*> ^ (@ q)) . 1 = y ) by FINSEQ_1:58;
assume A3: All x,p = All y,q ; :: thesis: ( x = y & p = q )
hence x = y by A1, A2, FINSEQ_1:46; :: thesis: p = q
<*x*> ^ (@ p) = <*y*> ^ (@ q) by A3, A1, FINSEQ_1:46;
hence p = q by A2, FINSEQ_1:46; :: thesis: verum