( x <> 0. L & y <> 0. L ) ;
then (y ") * y = 1. L by VECTSP_1:def 10;
then y " <> 0. L ;
hence x / y <> 0. L by VECTSP_2:def 1; :: according to STRUCT_0:def 12 :: thesis: verum