let L be non empty left_unital doubleLoopStr ; :: thesis: for p being sequence of L holds (1. L) * p = p
let p be sequence of L; :: thesis: (1. L) * p = p
set t = (1. L) * p;

now :: thesis: for x being object st x in NAT holds
((1. L) * p) . x = p . x

let x be object ; :: thesis: ( x in NAT implies ((1. L) * p) . x = p . x )
assume x in NAT ; :: thesis: ((1. L) * p) . x = p . x
then reconsider i = x as Element of NAT ;
thus ((1. L) * p) . x = (1. L) * (p . i) by POLYNOM5:def 4
.= p . x ; :: thesis: verum

end;

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