let K be non degenerated almost_left_invertible associative commutative well-unital doubleLoopStr ; :: 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 ; :: thesis: verum