1. L = (1. L) * (1. L) ;
hence ex b₁ being Element of L st b₁ is unital by GCD_1:def 2; :: thesis: verum