let L be non empty well-unital multLoopStr ; :: thesis: for p being sequence of L holds (1. L) * p = p
let p be sequence of L; :: thesis: (1. L) * p = p
for n being Element of NAT holds p . n = (1. L) * (p . n) ;
hence (1. L) * p = p by Def4; :: thesis: verum