for K being Field
for V being finite-dimensional VectSp of K
for W being Subspace of V ex S being Linear_Compl of W ex T being linear-transformation of S,(VectQuot (V,W)) st
( T is bijective & ( for v being Vector of V st v in S holds
T . v = v + W ) )