命題
M を n 次元多様体とする。
ω ∈ Ω^p(M) (>>315) とする。
X_1, ..., X_(p+1) ∈ X(M) (>>238) に対して、

dω(X_1, ..., X_(p+1)) = Σ(-1)^(i+1)X_iω(X_1, ..., (X_i)^, ..., X_(p+1))
+ Σ[i ＜ j](-1)^(i+j)X_iω([X_i, X_j], X_1, ..., (X_i)^, ..., (X_j)^, ..., X_(p+1))

証明
F(ω)(X_1, ..., X_(p+1)) = Σ(-1)^(i+1)X_iω(X_1, ..., (X_i)^, ..., X_(p+1))
+ Σ[i ＜ j](-1)^(i+j)X_iω([X_i, X_j], X_1, ..., (X_i)^, ..., (X_j)^, ..., X_(p+1))
とおく。

U を M の任意の座標近傍とし、(x_1, ..., x_n) をその局所座標とする。
U において ω = fdx_1Λdx_2Λ...Λdx_p として一般性を失わない。
ここで、f ∈ C^∞(U) である。

>>344より、U において
F(ω) = ΣF(ω)(∂/∂x_(i_1), ..., ∂/∂x_(i_(p+1))dx_(i_1)Λ...Λdx_(i_(p+1)) と書ける。
ここで、Σ は 1 ≦ i_1 ＜ ... ＜ i_(p+1) ≦ n となる組 (i_1, ..., i_(p+1)) 全体にわたる。

ω(∂/∂x_(i_1), ..., ∂/∂x_(i_p)) は
(i_1, ..., i_p) が (1, ..., p) の順列以外のとき 0 になる。
任意の i, j に対して [∂/∂x_i, ∂/∂x_j] = 0 である。

よって、
F(ω)(∂/∂x_(i_1), ..., ∂/∂x_(i_(p+1)) は
p ＜ j となる j に対して (i_1, ..., i_(p+1)) = (1, ..., p, j) となる場合以外は 0 である。
p ＜ j のとき、
F(ω)(∂/∂x_1, ..., ∂/∂x_p, ∂/∂x_j) = (-1)^p∂f/∂x_j

(続く)