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 ) )
assume A1: All x,p = All y,q ; :: thesis: ( x = y & p = q )
A2: ( (<*[3,0 ]*> ^ <*x*>) ^ (@ p) = <*[3,0 ]*> ^ (<*x*> ^ (@ p)) & (<*[3,0 ]*> ^ <*y*>) ^ (@ q) = <*[3,0 ]*> ^ (<*y*> ^ (@ q)) ) by FINSEQ_1:45;
then A3: <*x*> ^ (@ p) = <*y*> ^ (@ q) by A1, FINSEQ_1:46;
A4: ( (<*x*> ^ (@ p)) . 1 = x & (<*y*> ^ (@ q)) . 1 = y ) by FINSEQ_1:58;
hence x = y by A1, A2, FINSEQ_1:46; :: thesis: p = q
thus p = q by A3, A4, FINSEQ_1:46; :: thesis: verum