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