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