let K be non empty commutative left_unital multLoopStr ; :: thesis: 1. K is_a_unity_wrt the multF of K
set o = the multF of K;

now :: thesis: for h being Element of K holds
( the multF of K . ((1. K),h) = h & the multF of K . (h,(1. K)) = h )

let h be Element of K; :: thesis: ( the multF of K . ((1. K),h) = h & the multF of K . (h,(1. K)) = h )
thus the multF of K . ((1. K),h) = (1. K) * h
.= h ; :: thesis: the multF of K . (h,(1. K)) = h
thus the multF of K . (h,(1. K)) = h * (1. K)
.= h ; :: thesis: verum

end;

hence 1. K is_a_unity_wrt the multF of K by BINOP_1:3; :: thesis: verum