take {} V ; :: thesis: ( {} V is finite & {} V is linearly-independent )
thus ( {} V is finite & {} V is linearly-independent ) ; :: thesis: verum