for K being Field
for V1, V2 being VectSp of K
for A, B being Subset of V1
for L being Linear_Combination of V1 st Carrier L c= A \/ B & Sum L = 0. V1 holds
for f being additive homogeneous Function of V1,V2 st f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} holds
Carrier L c= A