Exterior derivative well-defined In a differential geometry book I am currently reading the exterior derivative for a k-form $\omega$ on a manifold is defined via coordinate-patches, that is given a chart $(U,x)$ and a coordinate representation of $\omega$ on $U$
$$\omega=\sum_{i_1<\cdots<i_k}a_{i_1...i_k}dx^{i_1}\wedge\cdots\wedge dx^{i_k}$$
the exterior derivative on $U$ is defined as 
$$d\omega=\sum_{i_1<\cdots<i_k}da_{i_1...i_k}\wedge dx^{i_1}\wedge\cdots\wedge 
dx^{i_k}$$
I want to convince myself that this definition for $d\omega$ is well defined, i.e. for a pair $(U,x),(V,y)$ of overlapping charts: 
$$\sum_{i_1<\cdots<i_k}da_{i_1...i_k}\wedge dx^{i_1}\wedge\cdots\wedge 
dx^{i_k}=\sum_{j_1<\cdots<j_k}db_{j_1...j_k}\wedge dy^{j_1}\wedge\cdots\wedge 
dy^{j_k}$$ on $U\cap V$, where $a_{i_1...i_k}$ and $b_{j_1...j_k}$ are the corresponding coefficient functions of $\omega$ with respect to $(U,x)$ and $(V,y)$. 
I tried plugging in the following transformation rules, but it got too messy:
$$b_{j_1...j_k}=\frac{\partial x^{i_1}}{\partial y_{j_1}}\cdots\frac{\partial x^{i_k}}{\partial y_{j_k}}a_{i_1...i_k}$$
$$dy^j=\frac{\partial y^{j}}{\partial x_{i}}dx^i$$
I would appreciate any help, thanks in advance!
Edit: I will try to outline my attempt so far: When I use $dy^j=\frac{\partial y^{j}}{\partial x_{i}}dx^i$ and $b_{j_1...j_k}=\frac{\partial x^{i_1}}{\partial y_{j_1}}\cdots\frac{\partial x^{i_k}}{\partial y_{j_k}}a_{i_1...i_k}$ on the right hand side and write $db_{j_1...j_k}=\frac{\partial}{\partial y_{j}}(b_{j_1...j_k})dy^j$, I would proceed by applying the product rule for k+1 factors. After that I am left with a lot of sums and I don't know how to go on. If it helps I could write out each step, but maybe someone knows an easier way than my brute force attempt?
 A: This computation is messy. However, there is a way to avoid it! It is not hard to convince oneself that $d$, as you define it, is the unique operator that eats $k$-forms and returns $k+1$-forms, which satisfies the following (intrinsic) requirements:
$1)$ It is $\mathbb{R}$-linear. That is, $d\lambda\omega=\lambda d\omega$ for any differential form $\omega$ and $\lambda\in\mathbb{R}$.
$2)$ For any function $f$, $df$ is the differential of $f$. That is, the $1$-form $df$ is given by $$df(X)=X(f).$$
$3)$ It satisfies the Leibniz rule $$d(\alpha\wedge\beta)=d\alpha\wedge\beta+(-1)^k\alpha\wedge d\beta,$$ where $k$ is the degree of $\alpha$.
$4)$ It squares to zero. That is, for any form $\omega$ we have $$dd\omega=0.$$ 
In addition, $d$ is clearly local, in the sense that if $\omega=\omega'$ in a neighborhood of $p$, then $d\omega(p)=d\omega'(p)$.
Now, you know that $d$ is well-defined on any coordinate chart, and on any intersection of such charts. So, by uniqueness, you can conclude that the different definitions on an intersection of coordinate charts all agree with one another.
