let L be non empty well-unital associative doubleLoopStr ; :: thesis: for p being sequence of L holds (1. L) * p = p
let p be sequence of L; :: thesis: (1. L) * p = p
for i being Element of NAT holds ((1. L) * p) . i = p . i

proof

let i be Element of NAT ; :: thesis: ((1. L) * p) . i = p . i
thus ((1. L) * p) . i = (1. L) * (p . i) by POLYNOM5:def 4
.= p . i ; :: thesis: verum

end;

hence (1. L) * p = p by FUNCT_2:63; :: thesis: verum