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

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