let K be Field; :: thesis: (1. K) " = 1. K
1. K <> 0. K ;
then ((1. K) ") * (1. K) = 1. K by VECTSP_1:def 10;
hence (1. K) " = 1. K by VECTSP_1:def 6; :: thesis: verum