let K be non empty commutative left_unital multLoopStr ; :: thesis: the_unity_wrt the multF of K = 1. K
reconsider e = 1. K as Element of K ;
e is_a_unity_wrt the multF of K by Th4;
hence the_unity_wrt the multF of K = 1. K by BINOP_1:def 8; :: thesis: verum