take {} the carrier of V ; :: thesis: {} the carrier of V is linearly-independent
thus {} the carrier of V is linearly-independent by Th7; :: thesis: verum