let K be Field; :: thesis: for V being finite-dimensional VectSp of K
for W being Subspace of V holds
( VectQuot (V,W) is finite-dimensional & (dim (VectQuot (V,W))) + (dim W) = dim V )
let V be finite-dimensional VectSp of K; :: thesis: for W being Subspace of V holds
( VectQuot (V,W) is finite-dimensional & (dim (VectQuot (V,W))) + (dim W) = dim V )
let W be Subspace of V; :: thesis: ( VectQuot (V,W) is finite-dimensional & (dim (VectQuot (V,W))) + (dim W) = dim V )
set Vq = VectQuot (V,W);
consider S being Linear_Compl of W, T being linear-transformation of S,(VectQuot (V,W)) such that
X1: T is bijective and
for v being Vector of V st v in S holds
T . v = v + W by Th38A;
( VectQuot (V,W) is finite-dimensional & dim S = dim (VectQuot (V,W)) ) by HM15, X1;
hence ( VectQuot (V,W) is finite-dimensional & (dim (VectQuot (V,W))) + (dim W) = dim V ) by VECTSP_5:def 5, VECTSP_9:34; :: thesis: verum