for x, y being Vector of ((0). V) holds x = y

proof

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

end;

hence (0). V is trivial ; :: thesis: verum