証明：行列と、数ベクトル空間から数ベクトル空間への一次写像。　　
　[永田『理系のための線形代数の基礎』(p.26-7);斎藤『線形代数入門』2章§3(pp.44-5);
　　佐武『線形代数学』�T§4(pp.17-19);志賀『線形代数30講』7講(pp.42-5)10講(p.63);
　　ホフマン・クンツェ『線形代数学I』3.4例13(p.91);;]
(舞台設定)
K：体（例：有理数をすべてあつめた集合Q、実数をすべて集めた集合R、複素数をすべてあつめた集合C）　
A：体K上の(m,n)型行列　
Kⁿ：体K上のn次元数ベクトル空間。　
　　すなわち、Kⁿ=K×K×…×K＝{ ( v₁, v₂, …, v_n )｜v₁∈Kかつv₂∈Kかつ…かつv_n∈K }に、
　　　　　　　　ベクトルの加法とスカラー乗法を定義したもの。　
　　ただし、Kⁿに属すすべての n次元数ベクトルは、 n次元縦ベクトルの形式で表されているものとする。
u,v：体Kからつくった n次元縦ベクトル。
K^m：体K上のm次元数ベクトル空間。　
　　　すなわち、K^m=K×K×…×K＝{ ( v₁, v₂, …, v_m )｜v₁∈Kかつv₂∈Kかつ…かつv_m∈K }に、
　　　　　　　　ベクトルの加法とスカラー乗法を定義したもの。　　　　　
　　ただし、K^mに属すすべての m次元数ベクトルは、 m次元縦ベクトルの形式で表されているものとする。
(定理の確認)
「体K上のn次元数ベクトル空間」Kⁿから
「体K上のm次元数ベクトル空間」K^mへの
任意の一次写像f:Kⁿ→K^mにたいして、　　　
　　(∀v∈Kⁿ) ( f (v)=(Av) )　
を満たす「体K上の(m,n)型行列」Aが一意的に存在する。

(証明)　
fを、任意の一次写像f:Kⁿ→K^mとおく。
また、「体K上のn次元数ベクトル空間」Kⁿの単位ベクトルを、e'₁, e'₂,…, e'_nとおく。
「体K上のm次元数ベクトル空間」K^mの単位ベクトルを、e₁, e₂,…, e_mとおく。
ただし、これらのすべての単位ベクトルは、縦ベクトルとして表す。　　
Step1:　
・写像f:Kⁿ→K^mとしたのだから、
　Kⁿの単位ベクトルのfによる像は、すべて、K^mに属す m次元数ベクトル（ただし縦）である。　
　すなわち、f ( e'₁ ) , f ( e'₂ ) , …, f ( e'_n ) ∈K^m 　…(1-1)
・K^mに属す m次元数ベクトルは、どれでも、
　K^mの単位ベクトルの一次結合として一意的に表せる。（∵）　
　ゆえに、(1-1)の、f ( e'₁ ) , f ( e'₂ ) , …, f ( e'_n ) ∈K^m も、すべて、
　K^mの単位ベクトルの一次結合として一意的に表せる。　
　つまり、
　　 f (e'₁)=a₁₁e₁＋a₂₁e₂＋…＋a_m1e_m 　　
　　 f (e'₂)=a₁₂e₁＋a₂₂e₂＋…＋a_m2e_m 　　
　　　：　　　　　：　
　　 f (e'_n)=a_1ne₁＋a_2ne₂＋…＋a_mne_m 　　
を満たす「体K上の(m,n)型行列」
　　　　
　が一意的に存在する。　…(1-2)　
　なお、上記を、成分を表に出して書くと、
　　　
　　　
　　　　：
　　　
　　　
　　　　　
　※　　　　　　
　　｜ f (e'₁)=a₁₁e₁＋a₂₁e₂＋…＋a_m1e_m
　　｜ f (e'₂)=a₁₂e₁＋a₂₂e₂＋…＋a_m2e_m 　　
　　｜　：　　　　　：　
　　｜ f (e'_n)=a_1ne₁＋a_2ne₂＋…＋a_mne_m 　　
　を、行列の乗法風に、
　　　　　　
　と書く、簡便法が、頻繁に用いられる。　
　この簡便法を用いると、上記の命題は、次のように、簡潔に表せる。　　　
　　　　　　｜　一次写像f:Kⁿ→K^mにたいして、
　　　　　　｜　　　　　　f (e'₁, e'₂, …, e'_n)=(e₁, e₂, …, e_m )A　　
　　　　　　｜　を満たす「体K上の(m,n)型行列」Aが一意的に存在する　　　　　　
Step2:
　Kⁿに属す n次元数ベクトルは、どれでも、
　Kⁿの単位ベクトルの一次結合として一意的に表せる。（∵）　
　ゆえに、任意の n次元数ベクトルv＝^t(v₁, v₂,…, v_n)∈Kⁿ も、
　Kⁿの単位ベクトルの一次結合として一意的に
　　　　v=v₁e'₁＋v₂e'₂＋…＋v_ne'_n　
　と表せる。　
Step3:
・Step2から
　任意のv＝^t(v₁, v₂,…, v_n)∈Kⁿ に対して、　
　　　　f (v)=f (v₁e'₁＋v₂e'₂＋…＋v_ne'_n)　　
・また、fは一次写像だから、
　　f (v₁e'₁＋v₂e'₂＋…＋v_ne'_n)=v₁ f (e'₁)＋v₂ f (e'₂)＋…＋v_n f (e'_n)　　　　（∵）　　
・以上２点をまとめると、
　任意のv＝^t(v₁, v₂,…, v_n)∈Kⁿ に対して、
　　　　f (v)=v₁ f (e'₁)＋v₂ f (e'₂)＋…＋v_n f (e'_n)　　
Step4:　　　　　　
・Step3の結果に、Step1-(1-2)の結果を繰り入れると、　　　　　
　任意のv∈Kⁿ に対して、
　f (v)=v₁ (a₁₁e₁＋a₂₁e₂＋…＋a_m1e_m )＋v₂ (a₁₂e₁＋a₂₂e₂＋…＋a_m2e_m )＋…＋v_n (a_1ne₁＋a_2ne₂＋…＋a_mne_m )　(※)　
　を満たす「体K上の(m,n)型行列」
　　　　
　が一意的に存在する
　といえる。　…(4-1)　
・(※)の右辺を整理すると次のようになる。　　
　v₁ (a₁₁e₁＋a₂₁e₂＋…＋a_m1e_m )＋v₂ (a₁₂e₁＋a₂₂e₂＋…＋a_m2e_m )＋…＋v_n (a_1ne₁＋a_2ne₂＋…＋a_mne_m )　　　
　= a₁₁v₁e₁＋a₂₁v₁e₂＋…＋a_m1v₁e_m＋a₁₂v₂e₁＋a₂₂v₂e₂＋…＋a_m2v₂e_m＋…＋a_1nv_ne₁＋a_2nv_ne₂＋…＋a_mnv_ne_m 　
　　　　∵数ベクトル空間で定義されたスカラー乗法のベクトルに関する分配則　
　=(a₁₁v₁＋a₁₂v₂＋…＋a_1nv_n )e₁＋ (a₂₁v₁＋a₂₂v₂＋…＋a_2nv_n )e₂＋…＋(a_m1v₁＋a_m2v₂＋…＋a_mnv_n )e_m　　　
　　　　∵数ベクトル空間で定義されたスカラー乗法のスカラーに関する分配則　
　　　∵単位ベクトルの定義とスカラー乗法の定義　　
　　=(Av)　　　　∵　行列の乗法の定義　
　　…(4-2)　
・(4-2)の結果を(4-1)に適用すると、
　任意のv∈Kⁿ に対して、
　f (v)=(Av)　　
　を満たす「体K上の(m,n)型行列」
　　　　
　が一意的に存在する
　となる。