for K being Ring
for V, U being VectSp of K
for f being linear-transformation of V,U ex T being linear-transformation of (VectQuot (V,(ker f))),(im f) st
( T = CQFunctional f & T is bijective )