take (0). V ; :: thesis: ( (0). V is finite-dimensional & (0). V is strict )
thus ( (0). V is finite-dimensional & (0). V is strict ) by Th6; :: thesis: verum