命題
M を n 次元多様体とする。
D を C^∞(M) (>>236)の微分(>>212)とする。

このとき D_X = D となる M 上のC^∞級ベクトル場 X が一意に存在する。
ここで、D_X は>>238で定義したものである。

証明
p を M の任意の点とする。
h を p の開近傍 U で定義されたC^∞級の実数値関数とする。
>>239より、M 上のC^∞級関数 f で p のある開近傍上で h = f となるものが存在する。
X_p(h) = D(f)(p) とおく。
>>242より、X_p(h) は f のとり方によらない。
D は微分だから X_p は p における接ベクトルである。
>>243より X はC^∞級ベクトル場である。

f ∈ C^∞(M) のとき Xf(p) = X_p(f) = D(f)(p)
よって、Xf = D(f)
即ち D_X = D である。

X の一意性は>>240で証明されている。
証明終