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: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