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 ZMODUL02:66;
hence x = y ; :: thesis: verum

end;

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