1. L = (1. L) * (1. L) ;
hence 1. L is unital ; :: thesis: verum