let A be QC-alphabet ; :: thesis: for x, y being bound_QC-variable of A
for p, q being Element of QC-WFF A st All (x,p) = All (y,q) holds
( x = y & p = q )
let x, y be bound_QC-variable of A; :: thesis: for p, q being Element of QC-WFF A st All (x,p) = All (y,q) holds
( x = y & p = q )
let p, q be Element of QC-WFF A; :: 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:32;
A2: ( (<*x*> ^ (@ p)) . 1 = x & (<*y*> ^ (@ q)) . 1 = y ) by FINSEQ_1:41;
assume A3: All (x,p) = All (y,q) ; :: thesis: ( x = y & p = q )
hence x = y by A1, A2, FINSEQ_1:33; :: thesis: p = q
<*x*> ^ (@ p) = <*y*> ^ (@ q) by A3, A1, FINSEQ_1:33;
hence p = q by A2, FINSEQ_1:33; :: thesis: verum