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

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 by VECTSP_1:def 19 ; :: thesis: the multF of K . h,(1. K) = h
thus the multF of K . h,(1. K) = h * (1. K)
.= h by VECTSP_1:def 19 ; :: thesis: verum

end;

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