let x, y be Vector of ((0). V); :: thesis: x = y
( x in (0). V & y in (0). V ) ;
then ( x = 0. V & y = 0. V ) by VECTSP_4:35;
hence x = y ; :: thesis: verum