定理 3.6
	φ : V -> V' : 同型対応

	a1,..,an in V が線型独立(従属) => φ(a1),..,φ(a_n) が独立(従属)
		# 実は、逆も言える

	prof)

		線型和 
		       c1a1+..+cnan = 0
		をφで移すとφの線型性より、
			φ(c1a1+..+cnan) = c1φ(a1)+..+cnφ(an) = φ(0) = 0
		つまり、前者が自明でない解があることと、移したさきが
		自明な解があることは同値となる。
		したがって、前者が独立 ( 自明解がない ) ならば、後者
		も独立 ( 自明解がない ) なる。

		従属の場合も同様である。

	「同型対応は、独立を独立に写し、従属を従属に移す」

定理 3.7
	V が n 個のベクトルあらなる基底を持てば、 V ≡ K^n となる。

	prof)
		<e1,..,en> を V の基底とする。
		all x in V exist! x1,..,xn in K
			s.t. x = x1e1 + .. + xnen
			# この x1,..,xn が x に対して一意的に存在
			# 存在 => 定義
			# 一意的 => 証明済(定理 ??)

		この関係を利用して、x in V と ( x1, .., xn ) in K^n を
		対応させるφを考えるとこれは、同型対応

			prof)
				φ(x) = ( x1,..,xn ) と置く
				# このφの線型性と全単射の性質を示す
				[線型性質]
					x + y = (x1+y1)e1+..+(xn+yn)en
					cx = (c x1)e1 + .. + (c xn)en
				を利用すると、
					φ(x+y) = φ(x) + φ(y) 
					φ(cx) = cφ(x)
				が言える。
				[全単射]
					(1 to 1)
						φ(x) = φ(y)
						      =>
					        (x1,..,xn) = (y1,..,yn)
						      =>
						x1 = y1, .., xn = yn
						      =>
						x = y

					( onto )

定理 3.8
	K^n において、m > n ならば、
		x1,..,xm は従属

		# 連立方程式の性質を利用する。

		## 利用しない方法もあるが、
		## それには準備が必要なので、後でやる。、

	特に、
		m != n => K^m != K^n

	Prof)
		[前半]
		K^n から m ( > n ) 個のベクトル a1,..,am を取り
			x1 a1 + .. + xm am = 0
		とき、成分毎に等式をたてる..

			x1 a11 + .. + xm am1 = 0
			x1 a12 + .. + xm am2 = 0
			   ...
			x1 a1n + .. + xm amn = 0

		この式は、x1 = .. = xn = 0 という自明な解を持つが、そ
		の他にも、「式の数 n が変数の数 m よりすくないので、自
		明な解が存在する」 ( これが、「連立方程式の性質」) ことが
		言える
			=> a1, .., am が従属である

			# 実は、この解全体のなす空間も線型空間になり、
			# その次元は、元の次元から、係数行列の次元を引
			# いたもの..
		
		[後半]
			今、K^m ≡ K^n とする。すると、あるφ : 同形対応
			が存在する。

			ここで、K^m から、基底 e1,..,em を取ると、それら
			は独立。
			そこで、φで移すと、φ(e1),..,φ(em) は、独立
			( 定理 3.7 ) よって前半より、m <= n
			同様に φ^-1 を利用すれば m >= n が成立するので
			これより m = n

定理 3.9
	K 上の線型空間 V が n このベクトルからなる基底をもてば、 n 個より
	大きなベクトルは従属
	特に、V の任意の基底は n 個のベクトルとなる。

	prof)
		(前半)
		[定理 3.7] より、V ≡ K^n なので、その同形対応をφとする
		a1,..,am in V ( m>n ) とすると、[定理 3.8] より、
		φ(a1),..,φ(am) は線型従属。よって、a1,..,an も線型
		従属 [定理 3.6]

		(後半)
		a1,..am in V が V の基底
			=> K^m ≡ V
		一方
			K^n ≡ V
		でもあったので、
			K^m ≡ V ≡ K^n
		より、
			K^m ≡ K^n
		つまり、
			m = n
		( by [定理 3.8] )

定義 (次元)
	V の基底がの個数 n を V の次元とよび dim V で表す。


# 連立方程式を利用しない、証明

定義
	S sub V ( S は有限集合 ) において
	S sub <e1,..,en> が S の極大線型独立系とは、
		1) e1,..,en が独立
		2) S の任意のげんが e1,..,em 線型和で表現できる
	とする。

3.10
	S sub V が、n 個の元よりなる極大線型独立系をもてば、n 個
	より多くの S のベクトルは線型従属である。

	特に S の任意の極大線型独立系は、n 個のベクトルよりなる。

	prof)
		# #S ( S の要素数 ) に関する帰納法でしめす。

		k = #S = 1 の時, Clear

		k - 1 で成立するとして、k を示す
			E = { e1, .., en } を S の極大独立系とする
			S sub F = { f1,..,fm } が線型独立とする。
			m <= n を示す
			E sub F なら Okey
			そうでないとすると.. fm not in E してよいので..
				S' = S - { fm }
			とする。すると #S = k - 1, よって、
			により、E は S' の極大独立系となる。
			F' = F - { fm } = {f1,..fm-1} も S' で独立

			帰納法の仮定より、
				m-1 <= n
			いま、
				m-1 = n

			とする(こうすると矛盾であることをしめす)。する
			と、帰納法の仮定により、F' は S' の極大線型独
			立系になる。

			e1,..,en は f1,..,fm-1 の線型結合で表せる
			更に、fm は e1,..,em で表せる
				=> fm は f1,..,fm-1 で表せる
					=> f1,..,fm が独立であるという仮定に矛盾
						=> m-1 != n つまり m - 1 < n
			よって、
				m <= n
						

定理 3.9 の別証明 ( 定理 3.8 つまり、連立方程式の性質を利用しない.. )
	E = <e1,..,en> : V の基底
	F = <f1,..,fm> : 線型独立

	今、S = E cup F とする。すると、[定理 3.10] より、
	E は、S の極大線型独立系よって、S に含まれる線型独立な
	ベクトルの集合のサイズは n 以下、つまり F も線型独立
	なベクトルの集合なので、そのサイズ m も n 以下、
	もし、F が基底ならば、同様にして、n も m 以下出しめせるので、
	m = n が言える。

	# 去年、「連立方程式の性質」を利用すれば、簡単だが、そうでない
	# 時の為に、他の方法も示した。

定理 3.11
	V, W が共に K 上の次元の等しい線型空間とすると、この二つの
	線型空間は、同形

	prof)
		dim V = dim M = n とすると、
			V ≡ K^n
			W ≡ K^n
		よって、
			V ≡ W

	# [注意] これまで V = { 0 } は除外して考えてきた、従って、
	# 今回までで、{ 0 } の次元は決っていない。

定義
	V = {0} の次元は 0


==

<<次元の例>>

	dim K^n = n
		dim V^2 = 2
		dim V^3 = 2

	dim Mmn(K) = mn
		prof)
			Eij = { e

	V = { x in K^n | Ax = の時 dim V = n - rank A

	P(K) : K 上の 1 変数多項式
		dim P(K) = 無限
	Pn(K) : n 次以下の多項式
		dim Pn(K) = n + 1

	V = { T : A -> K } ( V は A から K へ線型写像全体.. }
		#A = 無限 => #V = 無限
			prof)
				Ta(x) = 1 ( x  = a )
				      = 0 ( x != a )
				とすると、{ Ta | a in A } は独立
				つまり dim V > dim {Ta} = #A = 無限

		#A = n ( 有限の場合 ) => dim V = n
			<Ta1,..,Tan> が基底

	W = { [a,b] 上の連続関数 }

	V = { 実数列 }
	W = { 収束列 }
		共に、無限次元
			prof)
				ak = { 0, ..., 1, 0, .. }
					       ^ k 番目のみ 1 他は、0
				とすると、
					{ a1, .., ak, .. } は独立
				一方、	
					{ a1,.., } sub W sub V
				なので
					dim V > dim W < dim { a1, ..} = #N = 無限

	V = { {xn} | x_(n+k) + a_(n-1) x_(n-k-1) +..+ a0xn = 0 }
		=> dim V = n

                       x1     xn  xn+1..xn+k
		e1 = { 1, 0, ..0, -a0, .. }
		e2 = { 0, 1, ..0, -a0, .. }
			..
		en = { 0, 0, ..1, -a0, .. }
			# x1,..,xn を決めると自動的に xn+1,.. xn+k が解る
			# 漸化式を満すので..

		が基底としてとれる


	V = { y = f(x) | (d^k y)/(d x^k) + an-1(x) (d^(k-1) y)/(d x^(k-1))
			.. + a0(x)y = 0 }