let L be non empty associative well-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
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 3
.= p . i by VECTSP_1:def 19 ; :: thesis: verum

end;

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