let p, q be FinSequence of NAT ; :: thesis: for x, y being Variable st All (x,p) = All (y,q) holds
( x = y & p = q )
let x, y be Variable; :: thesis: ( All (x,p) = All (y,q) implies ( x = y & p = q ) )
A1: ( (<*4*> ^ <*x*>) ^ p = <*4*> ^ (<*x*> ^ p) & (<*4*> ^ <*y*>) ^ q = <*4*> ^ (<*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